1 files changed, 0 insertions, 66 deletions
diff --git a/examples/logic/ArithmEng.gf b/examples/logic/ArithmEng.gf
deleted file mode 100644
index 942b6d7c2..000000000
--- a/examples/logic/ArithmEng.gf
+++ /dev/null
@@ -1,66 +0,0 @@
---# -path=.:mathematical:present:prelude
-
-concrete ArithmEng of Arithm = LogicEng ** 
-  open
-    GrammarEng,
-    ParadigmsEng,
-    ProoftextEng,
-    MathematicalEng,
-    CombinatorsEng,
-    ConstructorsEng
-  in { 
-
-lin
-  Nat  = UseN  (regN "number") ;
-  Zero = UsePN (regPN "zero") ;
-  Succ = appN2 (regN2 "successor") ;
-
-  EqNat x y = mkS (predA2 (mkA2 (regA "equal") (mkPrep "to")) x y) ;
-  LtNat x y = mkS (predAComp (regA "equal") x y) ;
-  Div   x y = mkS (predA2 (mkA2 (regA "divisible") (mkPrep "by")) x y) ;
-  Even  x = mkS (predA (regA "even") x) ;
-  Odd   x = mkS (predA (regA "odd") x) ;
-  Prime x = mkS (predA (regA "prime") x) ;
-
-  one = UsePN (regPN "one") ;
-  two = UsePN (regPN "two") ;
-  sum = app (regN2 "sum") ;
-  prod = app (regN2 "product") ;
-
-  evax1 = 
-    proof (by (ref (mkLabel ["the first axiom of evenness ,"]))) 
-      (mkS (predA (regA "even") (UsePN (regPN "zero")))) ;
-  evax2 n c = 
-    appendText c 
-      (proof (by (ref (mkLabel ["the second axiom of evenness ,"]))) 
-        (mkS (predA (regA "odd") (appN2 (regN2 "successor") n)))) ;
-  evax3 n c = 
-    appendText c 
-      (proof (by (ref (mkLabel ["the third axiom of evenness ,"]))) 
-        (mkS (predA (regA "even") (appN2 (regN2 "successor") n)))) ;
-
-
-  eqax1 = 
-    proof (by (ref (mkLabel ["the first axiom of equality ,"]))) 
-      (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 (pred (mkA2 (regA "equal") (mkPrep "to")) 
-          (appN2 (regN2 "successor") m) (appN2 (regN2 "successor") n)))) ;
-
-  IndNat C d e = {s = 
-    ["we proceed by induction . for the basis ,"] ++ d.s ++ 
-    ["for the induction step, consider a number"] ++ C.$0 ++ 
-    ["and assume"] ++ C.s ++ 
-    --- "(" ++ e.$1 ++ ")" ++ 
-    "." ++ e.s ++ 
-    ["hence , for all numbers"] ++ C.$0 ++ "," ++ C.s ; lock_Text = <>} ;
-
-  ex1 = proof ["the first theorem and its proof"] ;
-
-} ;
-