changeset 9000 | c20d58286a51 |
parent 6349 | f7750d816c21 |
child 33615 | 261abc2e3155 |
--- a/src/HOL/Subst/ROOT.ML Tue May 30 16:03:09 2000 +0200 +++ b/src/HOL/Subst/ROOT.ML Tue May 30 16:08:38 2000 +0200 @@ -22,12 +22,6 @@ correctness and termination Unify - the unification function -To load, type use"ROOT.ML"; into an Isabelle-HOL that has TFL -also loaded. *) -writeln"Root file for Substitutions and Unification"; - -use_thy "Unify"; - -writeln"END: Root file for Substitutions and Unification"; +time_use_thy "Unify";