--- a/src/FOL/ex/nat2.thy Sat Apr 05 16:00:00 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-(* Title: FOL/ex/nat2.thy
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1991 University of Cambridge
-
-Theory for examples of simplification and induction on the natural numbers
-*)
-
-Nat2 = FOL +
-
-types nat 0
-arities nat :: term
-
-consts succ,pred :: "nat => nat"
- "0" :: "nat" ("0")
- "+" :: "[nat,nat] => nat" (infixr 90)
- "<","<=" :: "[nat,nat] => o" (infixr 70)
-
-rules
- pred_0 "pred(0) = 0"
- pred_succ "pred(succ(m)) = m"
-
- plus_0 "0+n = n"
- plus_succ "succ(m)+n = succ(m+n)"
-
- nat_distinct1 "~ 0=succ(n)"
- nat_distinct2 "~ succ(m)=0"
- succ_inject "succ(m)=succ(n) <-> m=n"
-
- leq_0 "0 <= n"
- leq_succ_succ "succ(m)<=succ(n) <-> m<=n"
- leq_succ_0 "~ succ(m) <= 0"
-
- lt_0_succ "0 < succ(n)"
- lt_succ_succ "succ(m)<succ(n) <-> m<n"
- lt_0 "~ m < 0"
-
- nat_ind "[| P(0); ALL n. P(n)-->P(succ(n)) |] ==> All(P)"
-end