equal
deleted
inserted
replaced
21 open Tactic; (* NONE *) |
21 open Tactic; (* NONE *) |
22 open P_Model; (* NONE *) |
22 open P_Model; (* NONE *) |
23 open Eval; get_pair; |
23 open Eval; get_pair; |
24 open TermC; atomt; |
24 open TermC; atomt; |
25 open Rule; ThmC.string_of_thm; |
25 open Rule; ThmC.string_of_thm; |
|
26 |
|
27 Know_Store.set_ref_last_thy @{theory}; |
|
28 (*otherwise ERRORs in pbl-met-hierarchy.sml, refine.sml, evaluate.sml*) |
26 \<close> |
29 \<close> |
27 ML_file "BaseDefinitions/libraryC.sml" |
|
28 |
30 |
29 section \<open>code for copy & paste ===============================================================\<close> |
31 section \<open>code for copy & paste ===============================================================\<close> |
30 ML \<open> |
32 ML \<open> |
31 "~~~~~ fun xxx , args:"; val () = (); |
33 "~~~~~ fun xxx , args:"; val () = (); |
32 "~~~~~ and xxx , args:"; val () = (); |
34 "~~~~~ and xxx , args:"; val () = (); |
50 print_statement "" |
52 print_statement "" |
51 print_theory |
53 print_theory |
52 ML_command \<open>Pretty.writeln prt\<close> |
54 ML_command \<open>Pretty.writeln prt\<close> |
53 declare [[ML_print_depth = 999]] |
55 declare [[ML_print_depth = 999]] |
54 declare [[ML_exception_trace]] |
56 declare [[ML_exception_trace]] |
55 \<close> |
|
56 ML \<open> |
|
57 (*========== inhibit exn WN130909 TODO ========================================================= |
|
58 ============ inhibit exn WN130909 TODO ========================================================*) |
|
59 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
|
60 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*) |
|
61 \<close> |
57 \<close> |
62 |
58 |
63 section \<open>===================================================================================\<close> |
59 section \<open>===================================================================================\<close> |
64 ML \<open> |
60 ML \<open> |
65 "~~~~~ fun xxx, args:"; val () = (); |
61 "~~~~~ fun xxx, args:"; val () = (); |