440 "----------- fun string_of_thmI for_[.]_) ------------------------"; |
440 "----------- fun string_of_thmI for_[.]_) ------------------------"; |
441 "----------- fun string_of_thmI for_[.]_) ------------------------"; |
441 "----------- fun string_of_thmI for_[.]_) ------------------------"; |
442 "----- these work ?!?"; |
442 "----- these work ?!?"; |
443 val th = sym_thm real_minus_eq_cancel; |
443 val th = sym_thm real_minus_eq_cancel; |
444 val Th = sym_Thm (Thm ("real_minus_eq_cancel", real_minus_eq_cancel)); |
444 val Th = sym_Thm (Thm ("real_minus_eq_cancel", real_minus_eq_cancel)); |
445 val th'= mk_thm Isac.thy ((de_quote o string_of_thm) real_minus_eq_cancel); |
445 val th'= mk_thm (theory "Isac") ((de_quote o string_of_thm) real_minus_eq_cancel); |
446 val th'= mk_thm Biegelinie.thy((de_quote o string_of_thm)real_minus_eq_cancel); |
446 val th'= mk_thm Biegelinie.thy((de_quote o string_of_thm)real_minus_eq_cancel); |
447 |
447 |
448 "----- DIFFERENCE TO ABOVE ?!?: this is still ok, when called in next_tac..."; |
448 "----- DIFFERENCE TO ABOVE ?!?: this is still ok, when called in next_tac..."; |
449 val ((pt,(p,p_)), _) = get_calc 1; show_pt pt; |
449 val ((pt,(p,p_)), _) = get_calc 1; show_pt pt; |
450 val Appl (Rewrite' (_,_,_,_,thm',_,_)) = |
450 val Appl (Rewrite' (_,_,_,_,thm',_,_)) = |
502 |
502 |
503 "----------- fun filter_appl_rews --------------------------------"; |
503 "----------- fun filter_appl_rews --------------------------------"; |
504 "----------- fun filter_appl_rews --------------------------------"; |
504 "----------- fun filter_appl_rews --------------------------------"; |
505 "----------- fun filter_appl_rews --------------------------------"; |
505 "----------- fun filter_appl_rews --------------------------------"; |
506 val f = str2term "a + z + 2*a + 3*z + 5 + 6"; |
506 val f = str2term "a + z + 2*a + 3*z + 5 + 6"; |
507 val thy = assoc_thy "Isac.thy"; |
507 val thy = assoc_thy "Isac"; |
508 val subst = [(*TODO.WN071231 test Rewrite_Inst*)]; |
508 val subst = [(*TODO.WN071231 test Rewrite_Inst*)]; |
509 val rls = Test_simplify; |
509 val rls = Test_simplify; |
510 (* val rls = rls_p_33; filter_appl_rews ---> length 2 |
510 (* val rls = rls_p_33; filter_appl_rews ---> length 2 |
511 val rls = norm_Poly; filter_appl_rews ---> length 1 |
511 val rls = norm_Poly; filter_appl_rews ---> length 1 |
512 *) |
512 *) |