equal
deleted
inserted
replaced
103 open Ctree; append_problem; |
103 open Ctree; append_problem; |
104 open Specify; show_ptyps; |
104 open Specify; show_ptyps; |
105 open Applicable; mk_set; |
105 open Applicable; mk_set; |
106 open Solve; (* NONE *) |
106 open Solve; (* NONE *) |
107 open Selem; e_fmz; |
107 open Selem; e_fmz; |
108 open Stool; transfer_asms_from_to; |
108 open Stool; (* NONE *) |
|
109 open ContextC; transfer_asms_from_to; |
109 open Tactic; (* NONE *) |
110 open Tactic; (* NONE *) |
110 open Model; (* NONE *) |
111 open Model; (* NONE *) |
111 open LTool; rule2stac; |
112 open LTool; rule2stac; |
112 open Rewrite; mk_thm; |
113 open Rewrite; mk_thm; |
113 open Calc; get_pair; |
114 open Calc; get_pair; |
145 ML_file "calcelems.sml" |
146 ML_file "calcelems.sml" |
146 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt -------------------------------- |
147 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt -------------------------------- |
147 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*) |
148 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*) |
148 ML_file "kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*) |
149 ML_file "kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*) |
149 ML_file "ProgLang/termC.sml" |
150 ML_file "ProgLang/termC.sml" |
|
151 ML_file "ProgLang/contextC.sml" |
150 ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *) |
152 ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *) |
151 ML_file "ProgLang/rewrite.sml" |
153 ML_file "ProgLang/rewrite.sml" |
152 ML_file "ProgLang/listC.sml" |
154 ML_file "ProgLang/listC.sml" |
153 ML_file "ProgLang/scrtools.sml" |
155 ML_file "ProgLang/scrtools.sml" |
154 ML_file "ProgLang/tools.sml" |
156 ML_file "ProgLang/tools.sml" |