--- a/src/FOL/ex/If.thy Wed Feb 24 11:55:52 2010 +0100
+++ b/src/FOL/ex/If.thy Mon Mar 01 13:40:23 2010 +0100
@@ -7,8 +7,7 @@
theory If imports FOL begin
-constdefs
- "if" :: "[o,o,o]=>o"
+definition "if" :: "[o,o,o]=>o" where
"if(P,Q,R) == P&Q | ~P&R"
lemma ifI: