| author | paulson |
| Tue, 03 Aug 1999 13:15:54 +0200 | |
| changeset 7165 | 8c937127fd8c |
| parent 6349 | f7750d816c21 |
| child 8732 | aef229ca5e77 |
| permissions | -rw-r--r-- |
(* Title: HOL/Lex/ROOT.ML ID: $Id$ Author: Tobias Nipkow Copyright 1998 TUM *) use_thy"AutoChopper"; use_thy"AutoChopper1"; use_thy"AutoMaxChop"; (* 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"RegExp2NA"; use_thy"RegExp2NAe"; use_thy"Scanner";