--- a/src/HOL/Import/ROOT.ML Sat Mar 03 22:38:53 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -(* Title: HOL/Import/ROOT.ML - Author: Sebastian Skalberg (TU Muenchen) -*) - -use_thys ["HOL4Compat", "HOL4Syntax"];