changeset 1351 | 4a960c012383 |
parent 1296 | ae31bb7774a7 |
child 1465 | 5d7a7e439cec |
--- a/src/HOL/Subst/ROOT.ML Tue Nov 21 12:41:52 1995 +0100 +++ b/src/HOL/Subst/ROOT.ML Tue Nov 21 12:43:09 1995 +0100 @@ -26,10 +26,7 @@ HOL_build_completed; (*Cause examples to fail if HOL did*) writeln"Root file for Substitutions and Unification"; -loadpath := ["Subst"]; use_thy "Unifier"; -make_chart (); (*make HTML chart*) - writeln"END: Root file for Substitutions and Unification";