src/FOLP/ex/If.thy
changeset 19796 d86e7b1fc472
parent 17480 fd19f77dcf60
child 25991 31b38a39e589
equal deleted inserted replaced
19795:746274ca400b 19796:d86e7b1fc472
     3 theory If
     3 theory If
     4 imports FOLP
     4 imports FOLP
     5 begin
     5 begin
     6 
     6 
     7 constdefs
     7 constdefs
     8   if :: "[o,o,o]=>o"
     8   "if" :: "[o,o,o]=>o"
     9   "if(P,Q,R) == P&Q | ~P&R"
     9   "if(P,Q,R) == P&Q | ~P&R"
    10 
    10 
    11 ML {* use_legacy_bindings (the_context ()) *}
    11 ML {* use_legacy_bindings (the_context ()) *}
    12 
    12 
    13 end
    13 end