src/FOL/.ifol.thy.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/.ifol.thy.ML	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,96 @@
+structure IFOL =
+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 (Pure.thy)
+ "IFOL"
+ ([("term", ["logic"])],
+  ["term"],
+  [(["o"], 0)],
+  [(["o"], ([], "logic"))],
+  [(["True", "False"], "o")],
+  Some (NewSext {
+   mixfix =
+    [Mixfix("(_)", "o => prop", "Trueprop", [0], 5),
+     Infixl("=", "['a,'a] => o", 50),
+     Mixfix("~ _", "o => o", "Not", [40], 40),
+     Infixr("&", "[o,o] => o", 35),
+     Infixr("|", "[o,o] => o", 30),
+     Infixr("-->", "[o,o] => o", 25),
+     Infixr("<->", "[o,o] => o", 25),
+     Binder("ALL ", "('a => o) => o", "All", 0, 10),
+     Binder("EX ", "('a => o) => o", "Ex", 0, 10),
+     Binder("EX! ", "('a => o) => o", "Ex1", 0, 10)],
+   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}))
+ [("refl", "a=a"),
+  ("subst", "[| a=b;  P(a) |] ==> P(b)"),
+  ("conjI", "[| P;  Q |] ==> P&Q"),
+  ("conjunct1", "P&Q ==> P"),
+  ("conjunct2", "P&Q ==> Q"),
+  ("disjI1", "P ==> P|Q"),
+  ("disjI2", "Q ==> P|Q"),
+  ("disjE", "[| P|Q;  P ==> R;  Q ==> R |] ==> R"),
+  ("impI", "(P ==> Q) ==> P-->Q"),
+  ("mp", "[| P-->Q;  P |] ==> Q"),
+  ("FalseE", "False ==> P"),
+  ("True_def", "True == False-->False"),
+  ("not_def", "~P == P-->False"),
+  ("iff_def", "P<->Q == (P-->Q) & (Q-->P)"),
+  ("ex1_def", "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"),
+  ("allI", "(!!x. P(x)) ==> (ALL x.P(x))"),
+  ("spec", "(ALL x.P(x)) ==> P(x)"),
+  ("exI", "P(x) ==> (EX x.P(x))"),
+  ("exE", "[| EX x.P(x);  !!x. P(x) ==> R |] ==> R"),
+  ("eq_reflection", "(x=y)   ==> (x==y)"),
+  ("iff_reflection", "(P<->Q) ==> (P==Q)")]
+
+val ax = get_axiom thy
+
+val refl = ax "refl"
+val subst = ax "subst"
+val conjI = ax "conjI"
+val conjunct1 = ax "conjunct1"
+val conjunct2 = ax "conjunct2"
+val disjI1 = ax "disjI1"
+val disjI2 = ax "disjI2"
+val disjE = ax "disjE"
+val impI = ax "impI"
+val mp = ax "mp"
+val FalseE = ax "FalseE"
+val True_def = ax "True_def"
+val not_def = ax "not_def"
+val iff_def = ax "iff_def"
+val ex1_def = ax "ex1_def"
+val allI = ax "allI"
+val spec = ax "spec"
+val exI = ax "exI"
+val exE = ax "exE"
+val eq_reflection = ax "eq_reflection"
+val iff_reflection = ax "iff_reflection"
+
+
+end
+end