622 l = [] = false; |
622 l = [] = false; |
623 nstep_up thy ptp sc E l Skip_ a v (*--> Appy (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...) |
623 nstep_up thy ptp sc E l Skip_ a v (*--> Appy (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...) |
624 BUT WE FIND IN THE CODE ABOVE IN next_tac:*) |
624 BUT WE FIND IN THE CODE ABOVE IN next_tac:*) |
625 ; |
625 ; |
626 (*----------------------------------------------------------------------------------------------*) |
626 (*----------------------------------------------------------------------------------------------*) |
627 if string_of_thmI @{thm rnorm_equation_add} = "~ ?b =!= 0 ==> (?a = ?b) = (?a + - 1 * ?b = 0)" |
627 if string_of_thmI @{thm rnorm_equation_add} = "<not> ?b =!= 0 ==> (?a = ?b) = (?a + - 1 * ?b = 0)" |
628 then () else error "string_of_thmI changed"; |
628 then () else error "string_of_thmI changed"; |
629 if string_of_thm @{thm rnorm_equation_add} = "~ ?b =!= 0 ==> (?a = ?b) = (?a + - 1 * ?b = 0)" |
629 if string_of_thm @{thm rnorm_equation_add} = "<not> ?b =!= 0 ==> (?a = ?b) = (?a + - 1 * ?b = 0)" |
630 then () else error "string_of_thm changed"; |
630 then () else error "string_of_thm changed"; |
631 (*----------------------------------------------------------------------------------------------*) |
631 (*----------------------------------------------------------------------------------------------*) |
632 ; |
632 ; |
633 (*SEARCH FOR THE ERROR WENT DOWN TO THE END OF THIS TEST, AND THEN UP TO HERE AGAIN*) |
633 (*SEARCH FOR THE ERROR WENT DOWN TO THE END OF THIS TEST, AND THEN UP TO HERE AGAIN*) |
634 "~~~~~ fun nxt_solv, args:"; val (tac_, is, (pt, pos as (p,p_))) = (tac_, is, ptp); |
634 "~~~~~ fun nxt_solv, args:"; val (tac_, is, (pt, pos as (p,p_))) = (tac_, is, ptp); |