3 files changed, 29 insertions, 10 deletions
diff --git a/examples/logic/LogicI.gf b/examples/logic/LogicI.gf
index c9c374622..182ed6ff5 100644
--- a/examples/logic/LogicI.gf
+++ b/examples/logic/LogicI.gf
@@ -16,11 +16,16 @@ lincat
   Text  = Section ;
 
 lin
+  ThmWithProof = theorem ;
+
   Disj A B = coord or_Conj A B ;
   Impl A B = coord ifthen_DConj A B ;
 
   Abs = mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet IndefArt) contradiction_N)) ;
 
+  Univ A B = 
+    mkS (mkAdv for_Prep (mkNP all_Predet (mkNP (mkDet IndefArt (mkCN A $0))))) B ;
+
   DisjIl A B a = proof a (proof afortiori (coord or_Conj A B)) ;
   DisjIr A B b = proof b (proof afortiori (coord or_Conj A B)) ;
 
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 ;
+
 }
diff --git a/examples/logic/ProoftextEng.gf b/examples/logic/ProoftextEng.gf
index 02ad3492f..9ccd7a410 100644
--- a/examples/logic/ProoftextEng.gf
+++ b/examples/logic/ProoftextEng.gf
@@ -1,12 +1,19 @@
 --# -path=.:mathematical:present:resource-1.0/api:prelude
 
-instance ProoftextEng of Prooftext = open 
-  LexTheoryEng, 
-  GrammarEng, 
-  SymbolicEng, 
-  SymbolEng, 
-  (C=ConstructX),
-  CombinatorsEng, 
-  ConstructorsEng in {
-  }
-  ;
+instance ProoftextEng of Prooftext = 
+  open 
+    LexTheoryEng, 
+    GrammarEng, 
+    SymbolicEng, 
+    SymbolEng, 
+    (C=ConstructX),
+    CombinatorsEng, 
+    ConstructorsEng,
+    (P=ParadigmsEng)
+  in {
+
+oper
+  mkLabel : Str -> Label = \s -> UsePN (P.regPN s) ;
+
+
+}