1 files changed, 0 insertions, 66 deletions
diff --git a/grammars/logic/Arithm.gf b/grammars/logic/Arithm.gf
deleted file mode 100644
index 2a91c5ed0..000000000
--- a/grammars/logic/Arithm.gf
+++ /dev/null
@@ -1,66 +0,0 @@
-abstract Arithm = Logic ** {
-
--- arithmetic
-fun 
-  Nat, Real  : Dom ;
-data
-  zero : Elem Nat ;
-  succ : Elem Nat -> Elem Nat ;
-fun
-  trunc : Elem Real -> Elem Nat ;
-
-  EqNat : (m,n : Elem Nat) -> Prop ;
-  LtNat : (m,n : Elem Nat) -> Prop ;
-  Div   : (m,n : Elem Nat) -> Prop ;
-  Even  : Elem Nat -> Prop ;
-  Odd   : Elem Nat -> Prop ;
-  Prime : Elem Nat -> Prop ;
-
-  one  : Elem Nat ;
-  two  : Elem Nat ;
-  sum  : (m,n : Elem Nat) -> Elem Nat ;
-  prod : (m,n : Elem Nat) -> Elem Nat ;
-data
-  evax1 : Proof (Even zero) ;
-  evax2 : (n : Elem Nat) -> Proof (Even n) -> Proof (Odd (succ n)) ;
-  evax3 : (n : Elem Nat) -> Proof (Odd n)  -> Proof (Even (succ n)) ;
-  eqax1 : Proof (EqNat zero zero) ;
-  eqax2 : (m,n : Elem Nat) -> Proof (EqNat m n) -> Proof (EqNat (succ m) (succ n)) ;
-fun
-  IndNat : (C : Elem Nat -> Prop) -> 
-             Proof (C zero) -> 
-             ((x : Elem Nat) -> Proof (C x) -> Proof (C (succ x))) -> 
-                Proof (Univ Nat C) ;
-
-def 
-  one = succ zero ;
-  two = succ one ;
-  sum m (succ n) = succ (sum m n) ;
-  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))) ;
-
-  Abs = Abs ;
-
-fun ex1 : Text ;
-def ex1 = 
-  ThmWithProof 
-    (Univ Nat (\x -> Disj (Even x) (Odd x))) 
-    (IndNat 
-       (\x -> Disj (Even x) (Odd x)) 
-       (DisjIl (Even zero) (Odd zero) evax1) 
-       (\x -> \h -> DisjE (Even x) (Odd x) (Disj (Even (succ x)) (Odd (succ x))) 
-         (Hypo (Disj (Even x) (Odd x)) h) 
-         (\a -> DisjIr (Even (succ x)) (Odd (succ x)) 
-            (evax2 x (Hypo (Even x) a))) 
-         (\b -> DisjIl (Even (succ x)) (Odd (succ x)) 
-            (evax3 x (Hypo (Odd x) b))
-         )
-       )
-     ) ;
-} ;