equal
deleted
inserted
replaced
116 open SpecifyNEW; |
116 open SpecifyNEW; |
117 open Step_Specify; |
117 open Step_Specify; |
118 open Step_Solve; |
118 open Step_Solve; |
119 open Step; |
119 open Step; |
120 open Solve; (* NONE *) |
120 open Solve; (* NONE *) |
121 open Selem; e_fmz; |
|
122 open Stool; (* NONE *) |
121 open Stool; (* NONE *) |
123 open ContextC; transfer_asms_from_to; |
122 open ContextC; transfer_asms_from_to; |
124 open Tactic; (* NONE *) |
123 open Tactic; (* NONE *) |
125 open Model; (* NONE *) |
124 open Model; (* NONE *) |
126 open Rewrite; |
125 open Rewrite; |
233 subsection \<open>further functionality alongside batch build sequence\<close> |
232 subsection \<open>further functionality alongside batch build sequence\<close> |
234 ML_file "MathEngBasic/thmC.sml" |
233 ML_file "MathEngBasic/thmC.sml" |
235 ML_file "MathEngBasic/rewrite.sml" |
234 ML_file "MathEngBasic/rewrite.sml" |
236 ML_file "MathEngBasic/model.sml" |
235 ML_file "MathEngBasic/model.sml" |
237 ML_file "MathEngBasic/mstools.sml" |
236 ML_file "MathEngBasic/mstools.sml" |
238 ML_file "MathEngBasic/specification-elems.sml" |
|
239 ML_file "MathEngBasic/tactic.sml" |
237 ML_file "MathEngBasic/tactic.sml" |
240 ML_file "MathEngBasic/ctree.sml" |
238 ML_file "MathEngBasic/ctree.sml" |
241 ML_file "MathEngBasic/calculation.sml" |
239 ML_file "MathEngBasic/calculation.sml" |
242 |
240 |
243 ML_file "Specify/ptyps.sml" (* requires setup from ptyps.thy *) |
241 ML_file "Specify/ptyps.sml" (* requires setup from ptyps.thy *) |