Up to index of Isabelle/FOLP/ex
(* $Id: If.thy,v 1.2 2005/09/18 12:25:49 wenzelm Exp $ *) 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