equal
deleted
inserted
replaced
|
1 theory Test_Theory imports "~~/src/Tools/isac/Knowledge/Rational" |
|
2 begin |
|
3 ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml" |
|
4 (* ATTENTION: tests with CalcTreeTest, CalcTree do NOT work here, because Thy_Info.get_theory |
|
5 requires session Isac, see ~~/test/Tools/isac/ADDTESTS/session-get_theory *) |
|
6 |
|
7 section {* code for copy & paste ===============================================================*} |
|
8 ML {* |
|
9 "~~~~~ fun , args:"; val () = (); |
|
10 "~~~~~ and , args:"; val () = (); |
|
11 |
|
12 "~~~~~ to return val:"; val () = (); |
|
13 |
|
14 *} |
|
15 text {* |
|
16 declare [[show_types]] |
|
17 declare [[show_sorts]] |
|
18 find_theorems "?a <= ?a" |
|
19 |
|
20 print_facts |
|
21 print_statement "" |
|
22 print_theory |
|
23 *} |
|
24 ML {* |
|
25 (*========== inhibit exn WN130909 TODO ========================================================= |
|
26 ============ inhibit exn WN130909 TODO ========================================================*) |
|
27 (*-.-.-.-.-. isolate response ad-hoc .-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
|
28 -.-.-.-.-.-. isolate response ad-hoc .-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*) |
|
29 *} |
|
30 |
|
31 section {* =================================================================*} |
|
32 ML {* |
|
33 *} ML {* |
|
34 *} ML {* |
|
35 *} ML {* |
|
36 *} ML {* |
|
37 *} ML {* |
|
38 *} ML {* |
|
39 *} |
|
40 section {* =================================================================*} |
|
41 ML {* |
|
42 *} ML {* |
|
43 *} ML {* |
|
44 *} ML {* |
|
45 *} ML {* |
|
46 *} ML {* |
|
47 *} ML {* |
|
48 *} ML {* |
|
49 *} |
|
50 section {* =================================================================*} |
|
51 ML {* |
|
52 *} ML {* |
|
53 *} ML {* |
|
54 *} ML {* |
|
55 *} ML {* |
|
56 *} ML {* |
|
57 *} ML {* |
|
58 *} ML {* |
|
59 *} |
|
60 |
|
61 end |
|
62 |
|
63 |