From 0c5f2c12880d339e51e5133c61216f233d5a9a7b Mon Sep 17 00:00:00 2001
From: aarne <aarne@cs.chalmers.se>
Date: Mon, 27 Nov 2006 21:03:15 +0000
Subject: more in ArithmEng

---
 examples/logic/LogicI.gf | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

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

diff --git a/examples/logic/LogicI.gf b/examples/logic/LogicI.gf
index 61d948607..09ffe661d 100644
--- a/examples/logic/LogicI.gf
+++ b/examples/logic/LogicI.gf
@@ -4,8 +4,7 @@ incomplete concrete LogicI of Logic =
     Prooftext, 
     Grammar, 
     Constructors, 
-    Combinators,
-    ParamX ---
+    Combinators
   in {
 
 lincat 
@@ -19,10 +18,12 @@ lincat
 lin
   ThmWithProof = theorem ;
 
+  Conj A B = coord and_Conj A B ;
   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)) ;
+  Abs = 
+    mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet IndefArt) contradiction_N)) ;
 
   Univ A B = 
     AdvS 
@@ -45,13 +46,14 @@ lin
         (proof therefore C)) ;
 
   ImplI A B b = 
-    proof (assumption A) (appendText b (proof therefore (coord ifthen_DConj A B))) ;
+    proof 
+      (assumption A) 
+      (appendText b (proof therefore (coord ifthen_DConj A B))) ;
 
   Hypoth A h = proof hypothesis A ;
 
 
---- this should not be here, but is needed for variables
 lindef
-  Elem s = {s = \\_ => s ; a = {n = Sg ; p = P3} ; lock_NP = <>} ;
+  Elem = defNP ;
 
-}
\ No newline at end of file
+}
-- 
cgit v1.2.3