| changeset 15338 | 08519594b0e4 |
| parent 15337 | 628d87767434 |
| child 15339 | a7b603bbc1e6 |
| 15337:628d87767434 | 15338:08519594b0e4 |
|---|---|
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(); |