From fd90fe0791961982570835582dc900627ee62cd5 Mon Sep 17 00:00:00 2001
From: aarne <aarne@cs.chalmers.se>
Date: Thu, 21 Dec 2006 09:25:02 +0000
Subject: overload rules and their documentation

---
 examples/logic/ArithmEng.gf | 8 ++++----
 examples/logic/LogicI.gf    | 2 +-
 examples/logic/Prooftext.gf | 2 +-
 3 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'examples')

diff --git a/examples/logic/ArithmEng.gf b/examples/logic/ArithmEng.gf
index 1ab4c2abd..21b68dd03 100644
--- a/examples/logic/ArithmEng.gf
+++ b/examples/logic/ArithmEng.gf
@@ -24,8 +24,8 @@ lin
 
   one = UsePN (regPN "one") ;
   two = UsePN (regPN "two") ;
-  sum = appColl (regN2 "sum") ;
-  prod = appColl (regN2 "product") ;
+  sum = app (regN2 "sum") ;
+  prod = app (regN2 "product") ;
 
   evax1 = 
     proof (by (ref (mkLabel ["the first axiom of evenness ,"]))) 
@@ -42,14 +42,14 @@ lin
 
   eqax1 = 
     proof (by (ref (mkLabel ["the first axiom of equality ,"]))) 
-      (mkS (predA2 (mkA2 (regA "equal") (mkPrep "to")) 
+      (mkS (pred (mkA2 (regA "equal") (mkPrep "to")) 
          (UsePN (regPN "zero")) 
          (UsePN (regPN "zero")))) ;
 
   eqax2 m n c = 
     appendText c 
       (proof (by (ref (mkLabel ["the second axiom of equality ,"]))) 
-        (mkS (predA2 (mkA2 (regA "equal") (mkPrep "to")) 
+        (mkS (pred (mkA2 (regA "equal") (mkPrep "to")) 
           (appN2 (regN2 "successor") m) (appN2 (regN2 "successor") n)))) ;
 
   IndNat C d e = {s = 
diff --git a/examples/logic/LogicI.gf b/examples/logic/LogicI.gf
index 1f9b08e41..3598022ac 100644
--- a/examples/logic/LogicI.gf
+++ b/examples/logic/LogicI.gf
@@ -28,7 +28,7 @@ lin
   Univ A B = 
     AdvS 
       (mkAdv for_Prep (mkNP all_Predet 
-        (mkNP (mkDet (PlQuant IndefArt) NoNum NoOrd) (mkCN A (symb B.$0)))))
+        (mkNP (mkDet (PlQuant IndefArt)) (mkCN A (symb B.$0)))))
       B ;
 
   DisjIl A B a = proof a (proof afortiori (coord or_Conj A B)) ;
diff --git a/examples/logic/Prooftext.gf b/examples/logic/Prooftext.gf
index 4c193740a..1833d6308 100644
--- a/examples/logic/Prooftext.gf
+++ b/examples/logic/Prooftext.gf
@@ -55,7 +55,7 @@ oper
     proof : Decl -> Proof
       = \d -> d ;
     proof : Proof -> Proof -> Proof
-      = \p,q -> appendText p q ;
+      = appendText ;
     proof : Branching -> Proofs -> Proof
       = \b,ps -> mkText (mkPhr b) ps
     } ;
-- 
cgit v1.2.3