13 "----------- change to parse ctxt -----------------------"; |
13 "----------- change to parse ctxt -----------------------"; |
14 "----------- debugging setContext..pbl_ -----------------"; |
14 "----------- debugging setContext..pbl_ -----------------"; |
15 "----------- tryrefine ----------------------------------"; |
15 "----------- tryrefine ----------------------------------"; |
16 "----------- search for Or_to_List ----------------------"; |
16 "----------- search for Or_to_List ----------------------"; |
17 "----------- check thy in CalcTreeTEST ------------------"; |
17 "----------- check thy in CalcTreeTEST ------------------"; |
18 "----------- identified error in fun getTactic, string_of_thmI ---------------"; |
18 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------"; |
19 "----------- improved fun getTactic for interSteps and numeral calculations --"; |
19 "----------- improved fun getTactic for interSteps and numeral calculations --"; |
20 "--------------------------------------------------------"; |
20 "--------------------------------------------------------"; |
21 "--------------------------------------------------------"; |
21 "--------------------------------------------------------"; |
22 "--------------------------------------------------------"; |
22 "--------------------------------------------------------"; |
23 |
23 |
169 "~~~~~ after fun some_spec:"; |
169 "~~~~~ after fun some_spec:"; |
170 val (dI, pI, mI) = some_spec ospec spec; |
170 val (dI, pI, mI) = some_spec ospec spec; |
171 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*) |
171 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*) |
172 val thy = assoc_thy dI; (*caused ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*) |
172 val thy = assoc_thy dI; (*caused ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*) |
173 |
173 |
174 "----------- identified error in fun getTactic, string_of_thmI ---------------"; |
174 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------"; |
175 "----------- identified error in fun getTactic, string_of_thmI ---------------"; |
175 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------"; |
176 "----------- identified error in fun getTactic, string_of_thmI ---------------"; |
176 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------"; |
177 reset_states (); |
177 reset_states (); |
178 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], |
178 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], |
179 ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))]; |
179 ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))]; |
180 moveActiveRoot 1; |
180 moveActiveRoot 1; |
181 autoCalculate 1 CompleteCalcHead; |
181 autoCalculate 1 CompleteCalcHead; |
232 l = [] = false; |
232 l = [] = false; |
233 go_scan_up thy ptp sc ist true (*--> Accept_Tac (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...) |
233 go_scan_up thy ptp sc ist true (*--> Accept_Tac (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...) |
234 BUT WE FIND IN THE CODE ABOVE IN find_next_step:*) |
234 BUT WE FIND IN THE CODE ABOVE IN find_next_step:*) |
235 ; |
235 ; |
236 (*----------------------------------------------------------------------------------------------*) |
236 (*----------------------------------------------------------------------------------------------*) |
237 if string_of_thmI @{thm rnorm_equation_add} = "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)" |
237 if ThmC.string_of_thm @{thm rnorm_equation_add} = "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)" |
238 then () else error "string_of_thmI changed"; |
238 then () else error "ThmC.string_of_thm changed"; |
239 if string_of_thm @{thm rnorm_equation_add} = "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)" |
239 if ThmC.string_of_thm @{thm rnorm_equation_add} = "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)" |
240 then () else error "string_of_thm changed"; |
240 then () else error "string_of_thm changed"; |
241 (*----------------------------------------------------------------------------------------------*) |
241 (*----------------------------------------------------------------------------------------------*) |
242 ; |
242 ; |
243 (*SEARCH FOR THE ERROR WENT DOWN TO THE END OF THIS TEST, AND THEN UP TO HERE AGAIN*) |
243 (*SEARCH FOR THE ERROR WENT DOWN TO THE END OF THIS TEST, AND THEN UP TO HERE AGAIN*) |
244 "~~~~~ fun begin_end_prog, args:"; val (tac_, is, (pt, pos as (p,p_))) = (tac_, is, ptp); |
244 "~~~~~ fun begin_end_prog, args:"; val (tac_, is, (pt, pos as (p,p_))) = (tac_, is, ptp); |