diff -r 4dc65845eab3 -r d8d7d1b785af src/FOLP/ex/If.thy --- 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: