(* Title: HOL/Import/HOL/ROOT.ML ID: $Id$ Author: Sebastian Skalberg (TU Muenchen) *) set show_types; set show_sorts; use_thy "HOL4Prob"; use_thy "HOL4";