changeset 1351 | 4a960c012383 |
parent 1300 | c7a8f374339b |
child 1925 | 1150f128c7fe |
--- a/src/HOL/MiniML/ROOT.ML Tue Nov 21 12:41:52 1995 +0100 +++ b/src/HOL/MiniML/ROOT.ML Tue Nov 21 12:43:09 1995 +0100 @@ -9,9 +9,6 @@ HOL_build_completed; (*Make examples fail if HOL did*) writeln"Root file for HOL/MiniML"; -loadpath := [".","MiniML"]; Unify.trace_bound := 20; time_use_thy "I"; - -make_chart (); (*make HTML chart*)