src/FOL/ex/.nat2.thy.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/.nat2.thy.ML	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,76 @@
+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