src/FOL/ex/If.thy
changeset 19796 d86e7b1fc472
parent 16417 9bc16273c2d4
child 31974 e81979a703a4
--- a/src/FOL/ex/If.thy	Tue Jun 06 19:24:05 2006 +0200
+++ b/src/FOL/ex/If.thy	Tue Jun 06 20:42:25 2006 +0200
@@ -9,8 +9,8 @@
 theory If imports FOL begin
 
 constdefs
-  if :: "[o,o,o]=>o"
-   "if(P,Q,R) == P&Q | ~P&R"
+  "if" :: "[o,o,o]=>o"
+  "if(P,Q,R) == P&Q | ~P&R"
 
 lemma ifI:
     "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)"