1 |
1 |
2 theory Test_Some imports Isac |
2 theory Test_Some imports Isac |
3 uses ("~~/test/Tools/isac/Interpret/calchead.sml") |
3 uses ("~~/test/Tools/isac/Interpret/inform.sml") |
4 begin |
4 begin |
5 use "~~/test/Tools/isac/Interpret/calchead.sml" |
5 use "~~/test/Tools/isac/Interpret/inform.sml" |
6 |
6 |
7 declare [[show_types]] |
7 declare [[show_types]] |
8 declare [[show_sorts]] |
8 declare [[show_sorts]] |
9 find_theorems "?a <= ?a" |
9 find_theorems "?a <= ?a" |
10 |
10 |
|
11 print_facts |
|
12 print_statement "" |
|
13 print_theory |
|
14 |
|
15 ML {* |
|
16 *} |
11 ML {* (*==================*) |
17 ML {* (*==================*) |
12 *} |
18 *} |
13 ML {* |
19 ML {* |
14 *} |
20 *} |
15 ML {* |
21 ML {* |
16 *} |
22 *} |
17 ML {* |
23 ML {* |
18 *} |
24 *} |
19 ML {* |
25 ML {* |
20 *} |
26 *} |
21 ML {* |
27 ML {* (*==================*) |
22 *} |
|
23 ML {* (*/==================\*) |
|
24 *} |
28 *} |
25 ML {* |
29 ML {* |
26 *} |
30 *} |
27 ML {* |
31 ML {* |
28 *} |
32 *} |
29 ML {* (*\==================/*) |
33 ML {* |
|
34 *} |
|
35 ML {* |
|
36 *} |
|
37 ML {* (*==================*) |
30 "~~~~~ fun , args:"; val () = (); |
38 "~~~~~ fun , args:"; val () = (); |
31 |
39 |
32 "~~~~~ to return val:"; val () = (); |
40 "~~~~~ to return val:"; val () = (); |
33 |
41 |
34 *} |
42 *} |
35 end |
43 end |
36 |
44 |
37 (*========== inhibit exn WN1130630 maximum example broken ========================= |
45 (*========== inhibit exn WN1130701 broken already in 2009-2 ======================= |
38 ============ inhibit exn WN1130630 maximum example broken =======================*) |
46 ============ inhibit exn WN1130701 broken already in 2009-2 =====================*) |
39 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================== |
47 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================== |
40 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*) |
48 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*) |
41 |
49 |
42 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
50 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
43 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) |
51 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) |