src/FOL/ex/.if.thy.ML

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