| 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)"