| author | paulson |
| Wed, 03 Dec 1997 10:50:02 +0100 | |
| changeset 4351 | 36b28f78ed1b |
| parent 4137 | 2ce2e659c2b1 |
| child 4712 | facfbbca7242 |
| permissions | -rw-r--r-- |
| 1465 | 1 |
(* Title: HOL/Lex/ROOT.ML |
| 1344 | 2 |
ID: $Id$ |
| 1465 | 3 |
Author: Tobias Nipkow |
| 1344 | 4 |
Copyright 1995 TUM |
5 |
*) |
|
6 |
||
| 1465 | 7 |
HOL_build_completed; (*Make examples fail if HOL did*) |
| 1344 | 8 |
|
9 |
use_thy"AutoChopper"; |
|
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
1465
diff
changeset
|
10 |
use_thy"AutoChopper1"; |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
1465
diff
changeset
|
11 |
use_thy"Regset_of_auto"; |