changeset 17480 | fd19f77dcf60 |
parent 0 | a5a9c433f639 |
child 19796 | d86e7b1fc472 |
--- a/src/FOLP/ex/If.thy Sat Sep 17 20:49:14 2005 +0200 +++ b/src/FOLP/ex/If.thy Sun Sep 18 14:25:48 2005 +0200 @@ -1,5 +1,13 @@ -If = FOLP + -consts if :: "[o,o,o]=>o" -rules - if_def "if(P,Q,R) == P&Q | ~P&R" +(* $Id$ *) + +theory If +imports FOLP +begin + +constdefs + if :: "[o,o,o]=>o" + "if(P,Q,R) == P&Q | ~P&R" + +ML {* use_legacy_bindings (the_context ()) *} + end