equal
deleted
inserted
replaced
61 ; |
61 ; |
62 if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "- 1 * ?z = - ?z" |
62 if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "- 1 * ?z = - ?z" |
63 then () else error "fun revert_sym_rule changed 1"; |
63 then () else error "fun revert_sym_rule changed 1"; |
64 |
64 |
65 val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy |
65 val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy |
66 (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus})) |
66 (Thm ("real_diff_minus", @{thm real_diff_minus})) |
67 ; |
67 ; |
68 if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + - 1 * ?b" |
68 if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + - 1 * ?b" |
69 then () else error "fun revert_sym_rule changed 2" |
69 then () else error "fun revert_sym_rule changed 2" |