author | wenzelm |
Mon, 16 Aug 1999 22:07:12 +0200 | |
changeset 7224 | e41e64476f9b |
parent 6349 | f7750d816c21 |
child 8732 | aef229ca5e77 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/Lex/ROOT.ML |
1344 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Tobias Nipkow |
4832 | 4 |
Copyright 1998 TUM |
1344 | 5 |
*) |
6 |
||
7 |
use_thy"AutoChopper"; |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
1465
diff
changeset
|
8 |
use_thy"AutoChopper1"; |
4712 | 9 |
use_thy"AutoMaxChop"; |
4907
0eb6730de30f
Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
4832
diff
changeset
|
10 |
(* Do not swap the next two use_thy's. |
4832 | 11 |
There is some interference, probably via claset() or simpset(). |
12 |
Or via ML-bound names of axioms that are overwritten? |
|
13 |
*) |
|
14 |
use_thy"RegSet_of_nat_DA"; |
|
5323 | 15 |
use_thy"RegExp2NA"; |
4907
0eb6730de30f
Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
4832
diff
changeset
|
16 |
use_thy"RegExp2NAe"; |
0eb6730de30f
Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
4832
diff
changeset
|
17 |
use_thy"Scanner"; |