src/FOLP/ex/If.thy
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 19796 d86e7b1fc472
child 25991 31b38a39e589
permissions -rw-r--r--
filtering out some package theorems

(* $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