src/FOLP/ex/If.thy

--- a/src/FOLP/ex/If.thy	Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/If.thy	Sun Sep 18 14:25:48 2005 +0200
@@ -1,5 +1,13 @@
-If = FOLP +
-consts  if     :: "[o,o,o]=>o"
-rules
-        if_def "if(P,Q,R) == P&Q | ~P&R"
+(* $Id$ *)
+
+theory If
+imports FOLP
+begin
+
+constdefs
+  if :: "[o,o,o]=>o"
+  "if(P,Q,R) == P&Q | ~P&R"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
 end