(* Title: HOL/Import/HOL/ROOT.ML ID: $Id$ Author: Sebastian Skalberg (TU Muenchen) *) with_path ".." use_thy "HOL4Compat"; with_path ".." use_thy "HOL4Syntax"; setmp quick_and_dirty true use_thy "HOL4Prob"; setmp quick_and_dirty true use_thy "HOL4";