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