658 "~~~~~ fun getTactic, args:"; val (cI, (p:pos')) = (1, ([1,1],Frm)); |
658 "~~~~~ fun getTactic, args:"; val (cI, (p:pos')) = (1, ([1,1],Frm)); |
659 val ((pt,_),_) = get_calc cI |
659 val ((pt,_),_) = get_calc cI |
660 val (form, tac, asms) = pt_extract (pt, p) |
660 val (form, tac, asms) = pt_extract (pt, p) |
661 val SOME ta = tac; |
661 val SOME ta = tac; |
662 "~~~~~ fun gettacticOK2xml, args:"; val ((cI:calcID), tac) = (cI, ta); |
662 "~~~~~ fun gettacticOK2xml, args:"; val ((cI:calcID), tac) = (cI, ta); |
|
663 val i = 2; |
663 "~~~~~ fun tac2xml, args:"; val (j, (Rewrite thm')) = (i, tac); |
664 "~~~~~ fun tac2xml, args:"; val (j, (Rewrite thm')) = (i, tac); |
664 "~~~~~ fun thm'2xml, args:"; val (j, ((ID, form) : thm'')) = ((j+i), thm'); |
665 "~~~~~ fun thm'2xml, args:"; val (j, ((ID, form) : thm'')) = ((j+i), thm'); |
665 ID = "rnorm_equation_add"; |
666 ID = "rnorm_equation_add"; |
666 @{thm rnorm_equation_add}; |
667 @{thm rnorm_equation_add}; |
667 (term2str o Thm.prop_of) form = "~ ?b =!= 0 ==> (?a = ?b) = (?a + -1 * ?b = 0)" |
668 (term2str o Thm.prop_of) form = "~ ?b =!= 0 ==> (?a = ?b) = (?a + -1 * ?b = 0)" |