--- a/src/FOL/ex/.nat2.thy.ML Sat Apr 05 16:00:00 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,76 +0,0 @@
-structure Nat2 =
-struct
-
-local
- val parse_ast_translation = []
- val parse_preproc = None
- val parse_postproc = None
- val parse_translation = []
- val print_translation = []
- val print_preproc = None
- val print_postproc = None
- val print_ast_translation = []
-in
-
-(**** begin of user section ****)
-
-(**** end of user section ****)
-
-val thy = extend_theory (FOL.thy)
- "Nat2"
- ([],
- [],
- [(["nat"], 0)],
- [(["nat"], ([], "term"))],
- [(["succ", "pred"], "nat => nat")],
- Some (NewSext {
- mixfix =
- [Delimfix("0", "nat", "0"),
- Infixr("+", "[nat,nat] => nat", 90),
- Infixr("<", "[nat,nat] => o", 70),
- Infixr("<=", "[nat,nat] => o", 70)],
- xrules =
- [],
- parse_ast_translation = parse_ast_translation,
- parse_preproc = parse_preproc,
- parse_postproc = parse_postproc,
- parse_translation = parse_translation,
- print_translation = print_translation,
- print_preproc = print_preproc,
- print_postproc = print_postproc,
- print_ast_translation = print_ast_translation}))
- [("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)")]
-
-val ax = get_axiom thy
-
-val pred_0 = ax "pred_0"
-val pred_succ = ax "pred_succ"
-val plus_0 = ax "plus_0"
-val plus_succ = ax "plus_succ"
-val nat_distinct1 = ax "nat_distinct1"
-val nat_distinct2 = ax "nat_distinct2"
-val succ_inject = ax "succ_inject"
-val leq_0 = ax "leq_0"
-val leq_succ_succ = ax "leq_succ_succ"
-val leq_succ_0 = ax "leq_succ_0"
-val lt_0_succ = ax "lt_0_succ"
-val lt_succ_succ = ax "lt_succ_succ"
-val lt_0 = ax "lt_0"
-val nat_ind = ax "nat_ind"
-
-
-end
-end