src/HOL/Lex/ROOT.ML
changeset 4137 2ce2e659c2b1
parent 1465 5d7a7e439cec
child 4712 facfbbca7242
--- a/src/HOL/Lex/ROOT.ML	Tue Nov 04 20:52:20 1997 +0100
+++ b/src/HOL/Lex/ROOT.ML	Wed Nov 05 09:08:35 1997 +0100
@@ -7,3 +7,5 @@
 HOL_build_completed;    (*Make examples fail if HOL did*)
 
 use_thy"AutoChopper";
+use_thy"AutoChopper1";
+use_thy"Regset_of_auto";