--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/FOLP/ex/If.thy Thu Sep 16 12:20:38 1993 +0200 @@ -0,0 +1,5 @@ +If = FOLP + +consts if :: "[o,o,o]=>o" +rules + if_def "if(P,Q,R) == P&Q | ~P&R" +end