src/HOL/Bali/ROOT.ML

"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
by the new simproc defColl_regroup. More precisely, the simproc pulls an
equation x=t (or t=x) out of a nest of conjunctions to the front where the
simp rule singleton_conj_conv(2) converts to "if".

(*  Title:      HOL/Bali/ROOT.ML
    ID:         $Id$
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen

The Hoare logic for Bali.
*)

use_thys ["AxExample", "AxSound", "AxCompl", "Trans"];