# HG changeset patch # User paulson # Date 929090060 -7200 # Node ID 852f9ed01a53d64e27703e2d742f516bc118119e # Parent a42849eeb67485775267f0bf60c657e5d670e57c no longer needs ../Lex diff -r a42849eeb674 -r 852f9ed01a53 src/HOL/UNITY/ROOT.ML --- a/src/HOL/UNITY/ROOT.ML Fri Jun 11 10:33:43 1999 +0200 +++ b/src/HOL/UNITY/ROOT.ML Fri Jun 11 10:34:20 1999 +0200 @@ -9,10 +9,9 @@ writeln"Root file for HOL/UNITY"; set proof_timing; +set HOL_quantifiers; -add_path "../Lex"; (*to find Prefix.thy*) - -time_use_thy"UNITY"; +time_use_thy "UNITY"; time_use_thy "Deadlock"; time_use_thy "WFair"; time_use_thy "Common";