115 "~~~~~ fun Test_Code.init_calc @{context} , args:"; val [(fmz, sp):Formalise.T] = [(fmz, (dI,pI,mI))]; |
115 "~~~~~ fun Test_Code.init_calc @{context} , args:"; val [(fmz, sp):Formalise.T] = [(fmz, (dI,pI,mI))]; |
116 (*val ((pt, p), tacis) =*) |
116 (*val ((pt, p), tacis) =*) |
117 Step_Specify.nxt_specify_init_calc ctxt (fmz, sp); |
117 Step_Specify.nxt_specify_init_calc ctxt (fmz, sp); |
118 "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp); |
118 "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp); |
119 (*val (_, hdl, (dI, pI, mI), pors, pctxt) =*) |
119 (*val (_, hdl, (dI, pI, mI), pors, pctxt) =*) |
120 initialise (fmz, (dI, pI, mI)); |
120 initialise ctxt (fmz, (dI, pI, mI)); |
121 "~~~~~ fun initialise , args:"; val (fmz, (dI, pI, mI)) = (fmz, (dI, pI, mI)); |
121 "~~~~~ fun initialise , args:"; val (fmz, (dI, pI, mI)) = (fmz, (dI, pI, mI)); |
122 val thy = ThyC.get_theory dI |
122 val thy = ThyC.get_theory dI |
123 val ctxt = Proof_Context.init_global thy; |
123 val ctxt = Proof_Context.init_global thy; |
124 (*if*) mI = ["no_met"](*else*); |
124 (*if*) mI = ["no_met"](*else*); |
125 val pors = Problem.from_store ctxt pI |> #ppc |> O_Model.init thy fmz; |
125 val pors = Problem.from_store ctxt pI |> #ppc |> O_Model.init thy fmz; |