|
wneuper@59465
|
1 |
theory Test_Some imports Isac.Build_Thydata
|
|
wneuper@59265
|
2 |
begin
|
|
wneuper@59472
|
3 |
ML \<open>
|
|
wneuper@59265
|
4 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
|
|
wneuper@59417
|
5 |
(* these vvv test, if funs are intermediately opened in structure
|
|
wneuper@59417
|
6 |
in case of errors here consider ~~/./xtest-to-coding.sh *)
|
|
wneuper@59265
|
7 |
open Kernel;
|
|
wneuper@59265
|
8 |
open Math_Engine; CalcTreeTEST;
|
|
wneuper@59265
|
9 |
open Lucin; appy;
|
|
wneuper@59265
|
10 |
open Inform; cas_input;
|
|
wneuper@59265
|
11 |
open Rtools; trtas2str;
|
|
wneuper@59265
|
12 |
open Chead; pt_extract;
|
|
wneuper@59316
|
13 |
open Generate; (* NONE *)
|
|
wneuper@59276
|
14 |
open Ctree; append_problem;
|
|
wneuper@59269
|
15 |
open Specify; show_ptyps;
|
|
wneuper@59316
|
16 |
open Applicable; mk_set;
|
|
wneuper@59316
|
17 |
open Solve; (* NONE *)
|
|
wneuper@59308
|
18 |
open Selem; e_fmz;
|
|
wneuper@59308
|
19 |
open Stool; transfer_asms_from_to;
|
|
wneuper@59316
|
20 |
open Tac; (* NONE *)
|
|
wneuper@59316
|
21 |
open Model; (* NONE *)
|
|
wneuper@59417
|
22 |
open LTool; rule2stac;
|
|
wneuper@59417
|
23 |
open Rewrite; mk_thm;
|
|
wneuper@59417
|
24 |
open Calc; get_pair;
|
|
wneuper@59417
|
25 |
open TermC; atomt;
|
|
wneuper@59417
|
26 |
open Celem; e_pbt;
|
|
wneuper@59417
|
27 |
open Rule; string_of_thm;
|
|
wneuper@59531
|
28 |
open Tools; eval_lhs;
|
|
wneuper@59265
|
29 |
(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
|
wneuper@59472
|
30 |
\<close>
|
|
wneuper@59540
|
31 |
ML_file "Knowledge/biegelinie-3.sml"
|
|
neuper@48765
|
32 |
|
|
wneuper@59472
|
33 |
section \<open>code for copy & paste ===============================================================\<close>
|
|
wneuper@59472
|
34 |
ML \<open>
|
|
wneuper@59535
|
35 |
"~~~~~ fun xxx , args:"; val () = ();
|
|
wneuper@59535
|
36 |
"~~~~~ and xxx , args:"; val () = ();
|
|
neuper@48891
|
37 |
|
|
wneuper@59489
|
38 |
"~~~~~ to xxx return val:"; val () = ();
|
|
neuper@42398
|
39 |
|
|
wneuper@59472
|
40 |
\<close>
|
|
wneuper@59472
|
41 |
text \<open>
|
|
neuper@52101
|
42 |
declare [[show_types]]
|
|
neuper@55405
|
43 |
declare [[show_sorts]]
|
|
neuper@52101
|
44 |
find_theorems "?a <= ?a"
|
|
neuper@52101
|
45 |
|
|
wneuper@59230
|
46 |
print_theorems
|
|
neuper@52101
|
47 |
print_facts
|
|
neuper@52101
|
48 |
print_statement ""
|
|
neuper@52101
|
49 |
print_theory
|
|
wneuper@59230
|
50 |
ML_command \<open>Pretty.writeln prt\<close>
|
|
wneuper@59230
|
51 |
declare [[ML_print_depth = 999]]
|
|
wneuper@59252
|
52 |
declare [[ML_exception_trace]]
|
|
wneuper@59472
|
53 |
\<close>
|
|
wneuper@59472
|
54 |
ML \<open>
|
|
neuper@52105
|
55 |
(*========== inhibit exn WN130909 TODO =========================================================
|
|
neuper@52105
|
56 |
============ inhibit exn WN130909 TODO ========================================================*)
|
|
neuper@52101
|
57 |
(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
|
|
neuper@52101
|
58 |
-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*)
|
|
wneuper@59472
|
59 |
\<close>
|
|
neuper@52101
|
60 |
|
|
wneuper@59494
|
61 |
section \<open>===================================================================================\<close>
|
|
wneuper@59472
|
62 |
ML \<open>
|
|
wneuper@59494
|
63 |
"~~~~~ fun xxx, args:"; val () = ();
|
|
wneuper@59472
|
64 |
\<close> ML \<open>
|
|
wneuper@59472
|
65 |
\<close> ML \<open>
|
|
wneuper@59489
|
66 |
\<close> ML \<open>
|
|
wneuper@59494
|
67 |
"~~~~~ fun xxx, args:"; val () = ();
|
|
wneuper@59492
|
68 |
\<close>
|
|
wneuper@59492
|
69 |
|
|
wneuper@59533
|
70 |
section \<open>===================================================================================\<close>
|
|
wneuper@59472
|
71 |
ML \<open>
|
|
wneuper@59533
|
72 |
"~~~~~ fun xxx , args:"; val () = ();
|
|
wneuper@59517
|
73 |
\<close> ML \<open>
|
|
wneuper@59517
|
74 |
\<close> ML \<open>
|
|
wneuper@59517
|
75 |
\<close> ML \<open>
|
|
wneuper@59531
|
76 |
"~~~~~ fun xxx , args:"; val () = ();
|
|
wneuper@59517
|
77 |
\<close>
|
|
wneuper@59517
|
78 |
|
|
wneuper@59517
|
79 |
section \<open>===================================================================================\<close>
|
|
wneuper@59517
|
80 |
ML \<open>
|
|
wneuper@59531
|
81 |
"~~~~~ fun xxx , args:"; val () = ();
|
|
wneuper@59517
|
82 |
\<close> ML \<open>
|
|
wneuper@59517
|
83 |
\<close> ML \<open>
|
|
wneuper@59517
|
84 |
\<close> ML \<open>
|
|
wneuper@59531
|
85 |
"~~~~~ fun xxx , args:"; val () = ();
|
|
wneuper@59517
|
86 |
\<close>
|
|
wneuper@59517
|
87 |
|
|
wneuper@59535
|
88 |
section \<open>code for copy & paste ===============================================================\<close>
|
|
wneuper@59535
|
89 |
ML \<open>
|
|
wneuper@59531
|
90 |
"~~~~~ fun xxx , args:"; val () = ();
|
|
wneuper@59531
|
91 |
"~~~~~ and xxx , args:"; val () = ();
|
|
neuper@55279
|
92 |
|
|
wneuper@59535
|
93 |
"~~~~~ to xxx return val:"; val () = ();
|
|
wneuper@59535
|
94 |
\<close>
|
|
neuper@41943
|
95 |
end
|