src/HOL/Lex/ROOT.ML
changeset 8732 aef229ca5e77
parent 6349 f7750d816c21
child 9000 c20d58286a51
     1.1 --- a/src/HOL/Lex/ROOT.ML	Mon Apr 17 14:27:10 2000 +0200
     1.2 +++ b/src/HOL/Lex/ROOT.ML	Tue Apr 18 00:36:02 2000 +0200
     1.3 @@ -7,11 +7,5 @@
     1.4  use_thy"AutoChopper";
     1.5  use_thy"AutoChopper1";
     1.6  use_thy"AutoMaxChop";
     1.7 -(* Do not swap the next two use_thy's.
     1.8 -   There is some interference, probably via claset() or simpset().
     1.9 -   Or via ML-bound names of axioms that are overwritten?
    1.10 -*)
    1.11  use_thy"RegSet_of_nat_DA";
    1.12 -use_thy"RegExp2NA";
    1.13 -use_thy"RegExp2NAe";
    1.14  use_thy"Scanner";