(* Title: HOL/Import/ROOT.ML ID: $Id$ Author: Sebastian Skalberg (TU Muenchen) *) proofs := 0; use_thy "HOL4Compat"; use_thy "HOL4Syntax";