--- a/src/FOLP/ex/If.thy Tue Jun 06 19:24:05 2006 +0200
+++ b/src/FOLP/ex/If.thy Tue Jun 06 20:42:25 2006 +0200
@@ -5,7 +5,7 @@
begin
constdefs
- if :: "[o,o,o]=>o"
+ "if" :: "[o,o,o]=>o"
"if(P,Q,R) == P&Q | ~P&R"
ML {* use_legacy_bindings (the_context ()) *}