src/FOLP/ex/If.thy
changeset 35416 d8d7d1b785af
parent 25991 31b38a39e589
child 35762 af3ff2ba4c54
--- a/src/FOLP/ex/If.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/FOLP/ex/If.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -4,8 +4,7 @@
 imports FOLP
 begin
 
-constdefs
-  "if" :: "[o,o,o]=>o"
+definition "if" :: "[o,o,o]=>o" where
   "if(P,Q,R) == P&Q | ~P&R"
 
 lemma ifI: