formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
(* Title: HOL/IMP/ROOT.ML
ID: $Id$
Author: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow, David von Oheimb
Copyright 1995 TUM
Caveat: HOLCF/IMP depends on HOL/IMP
*)
use_thys ["Expr", "Transition", "VC", "Hoare_Den", "Examples", "Compiler0", "Compiler", "Live"];