src/FOL/.fol.thy.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/.fol.thy.ML	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,35 @@
+structure FOL =
+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 (IFOL.thy)
+ "FOL"
+ ([],
+  [],
+  [],
+  [],
+  [],
+  None)
+ [("classical", "(~P ==> P) ==> P")]
+
+val ax = get_axiom thy
+
+val classical = ax "classical"
+
+
+end
+end