From 854fe0aac10c56372f2e185ab9b68379c232d33b Mon Sep 17 00:00:00 2001
From: aarne <aarne@cs.chalmers.se>
Date: Mon, 27 Nov 2006 16:21:27 +0000
Subject: AdvS and for_Prep in resource (except Russian)

---
 examples/logic/Prooftext.gf | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'examples/logic/Prooftext.gf')

diff --git a/examples/logic/Prooftext.gf b/examples/logic/Prooftext.gf
index e6a6c710c..3a5a61894 100644
--- a/examples/logic/Prooftext.gf
+++ b/examples/logic/Prooftext.gf
@@ -34,6 +34,9 @@ oper
     = \decl,a,b -> 
         appendText decl (mkUtt (mkS (pred b a))) ;
 
+  theorem : Prop -> Proof -> Section 
+    = \prop,prf -> appendText (mkText (mkPhr prop) TEmpty) prf ;
+
   assumption : Prop -> Decl 
     = \p -> 
         mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS p)))) TEmpty ;
@@ -45,6 +48,8 @@ oper
   proof = overload {
     proof : Prop -> Proof 
       = \p -> mkText (mkPhr p) TEmpty ;
+    proof : Str -> Proof
+      = \s -> {s = s ++ "." ; lock_Text = <>} ;
     proof : Adverb -> Prop -> Proof
       = \a,p -> mkText (mkPhr a (mkUtt p) NoVoc) TEmpty ;
     proof : Decl -> Proof
@@ -76,4 +81,6 @@ oper
   refs : Refs -> Ref
     = \rs -> mkNP and_Conj rs ;
 
+  mkLabel : Str -> Label ;
+
 }
-- 
cgit v1.2.3