author | paulson |
Thu, 20 Feb 2003 11:09:48 +0100 | |
changeset 13824 | e4d8dea6dfc2 |
parent 5851 | 15ce4c1c8313 |
permissions | -rw-r--r-- |
5851 | 1 |
use_thy "ABexp"; |
2 |
use"abgoalind.ML"; |
|
3 |
use"autotac.ML"; |
|
4 |
result(); |
|
5 |
||
6 |
use_thy "Term"; |
|
7 |
use"tidproof.ML"; |
|
8 |
result(); |
|
9 |
use"appmap.ML"; |
|
10 |
by(induct_tac "ts" 1); |
|
11 |
by(Auto_tac); |
|
12 |
qed"subst_App_map"; |
|
13 |
Addsimps [subst_App_map]; |
|
14 |
result(); |
|
15 |
||
16 |
use_thy"Trie"; |
|
17 |
use"lookupempty.ML"; |
|
18 |
qed "lookup_empty"; |
|
19 |
Addsimps [lookup_empty]; |
|
20 |
use"trieAdds.ML"; |
|
21 |
use"triemain.ML"; |
|
22 |
use"trieinduct.ML"; |
|
23 |
use"trieexhaust.ML"; |
|
24 |
by(Auto_tac); |
|
25 |
result(); |