changeset 4907 | 0eb6730de30f |
parent 4832 | bc11b5b06f87 |
child 5323 | 028e00595280 |
--- a/src/HOL/Lex/ROOT.ML Fri May 08 15:45:01 1998 +0200 +++ b/src/HOL/Lex/ROOT.ML Fri May 08 18:33:29 1998 +0200 @@ -9,10 +9,10 @@ use_thy"AutoChopper"; use_thy"AutoChopper1"; use_thy"AutoMaxChop"; -(* Do no swap the next 2. +(* Do not swap the next two use_thy's. There is some interference, probably via claset() or simpset(). Or via ML-bound names of axioms that are overwritten? *) use_thy"RegSet_of_nat_DA"; -use_thy"NAe_of_RegExp"; -use_thy"Automata"; +use_thy"RegExp2NAe"; +use_thy"Scanner";