5377
|
1 |
use_thy "Tree";
|
|
2 |
|
|
3 |
context Main.thy;
|
|
4 |
use"exhaust.ML";
|
|
5 |
use"autotac.ML";
|
|
6 |
result();
|
|
7 |
|
|
8 |
use_thy"NatSum";
|
|
9 |
result();
|
|
10 |
|
|
11 |
use_thy"Types";
|
|
12 |
use_thy"Defs";
|
|
13 |
use_thy"ConstDefs";
|
|
14 |
|
|
15 |
context Main.thy;
|
|
16 |
Goal "! xs. if xs = [] then rev xs = [] else rev xs ~= []";
|
|
17 |
use"splitif.ML";
|
|
18 |
|
|
19 |
Goal "(case xs of [] => zs | y#ys => y#(ys@zs)) = xs@zs";
|
|
20 |
use"splitlist.ML";
|
|
21 |
|
|
22 |
use_thy "Itrev";
|
|
23 |
use "itrev1.ML";
|
|
24 |
use "itrev2.ML";
|
|
25 |
use "itrev3.ML";
|
|
26 |
use "induct_auto.ML";
|
|
27 |
result();
|