From 9d07bd92a87705a61d23e44cdbd659f08b055de5 Mon Sep 17 00:00:00 2001
From: aarne <unknown>
Date: Mon, 9 Aug 2004 13:22:59 +0000
Subject: small adjustments in grs

---
 grammars/logic/Arithm.gf | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'grammars')

diff --git a/grammars/logic/Arithm.gf b/grammars/logic/Arithm.gf
index e3ae706a4..7674e9551 100644
--- a/grammars/logic/Arithm.gf
+++ b/grammars/logic/Arithm.gf
@@ -34,16 +34,18 @@ fun
 def 
   one = succ zero ;
   two = succ one ;
-  sum m zero = m ;
   sum m (succ n) = succ (sum m n) ;
-  prod m zero = zero ;
+  sum m zero = m ;
   prod m (succ n) = sum (prod m n) m ;
+  prod m zero = zero ;
   LtNat m n = Exist Nat (\x -> EqNat n (sum m (succ x))) ;
   Div m n = Exist Nat (\x -> EqNat m (prod x n)) ;
   Prime n = Conj 
               (LtNat one n) 
               (Univ Nat (\x -> Impl (Conj (LtNat one x) (Div n x)) (EqNat x n))) ;
 
+--- data Elem = zero | succ ;
+
 fun ex1 : Text ;
 def ex1 = 
   ThmWithProof 
-- 
cgit v1.2.3