46 "----------- fun revert_sym_rule ---------------------------------------------------------------"; |
46 "----------- fun revert_sym_rule ---------------------------------------------------------------"; |
47 "----------- fun revert_sym_rule ---------------------------------------------------------------"; |
47 "----------- fun revert_sym_rule ---------------------------------------------------------------"; |
48 "~~~~~ fun revert_sym_rule , args:"; val (thy, (Rule.Thm (id, thm))) = |
48 "~~~~~ fun revert_sym_rule , args:"; val (thy, (Rule.Thm (id, thm))) = |
49 (@{theory Isac_Knowledge}, \<^rule_thm_sym>\<open>real_mult_minus1\<close>); |
49 (@{theory Isac_Knowledge}, \<^rule_thm_sym>\<open>real_mult_minus1\<close>); |
50 |
50 |
51 if id = "sym_real_mult_minus1" andalso ThmC.string_of_thm thm = "- ?z1 = -1 * ?z1" then () |
51 if id = "sym_real_mult_minus1" andalso ThmC.string_of_thm thm = "- ?z1 = - 1 * ?z1" then () |
52 else error "input to revert_sym_rule CHANGED"; |
52 else error "input to revert_sym_rule CHANGED"; |
53 |
53 |
54 (*if*) is_sym (cut_id id) (*then*); |
54 (*if*) is_sym (cut_id id) (*then*); |
55 val id' = id_drop_sym id |
55 val id' = id_drop_sym id |
56 val thm' = thm_from_thy thy id' |
56 val thm' = thm_from_thy thy id' |
57 val id'' = Thm.get_name_hint thm' |
57 val id'' = Thm.get_name_hint thm' |
58 |
58 |
59 val thy = @{theory Isac_Knowledge} |
59 val thy = @{theory Isac_Knowledge} |
60 val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy (\<^rule_thm_sym>\<open>real_mult_minus1\<close>) |
60 val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy (\<^rule_thm_sym>\<open>real_mult_minus1\<close>) |
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", ThmC.numerals_to_Free @{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" |