equal
deleted
inserted
replaced
63 |
63 |
64 fun id_of_thm thm = thm |> Thm.get_name_hint |> cut_id; |
64 fun id_of_thm thm = thm |> Thm.get_name_hint |> cut_id; |
65 fun of_thm thm = (id_of_thm thm, thm); |
65 fun of_thm thm = (id_of_thm thm, thm); |
66 fun from_rule _ (Rule.Thm (id, thm)) = (id, thm) |
66 fun from_rule _ (Rule.Thm (id, thm)) = (id, thm) |
67 | from_rule ctxt r = |
67 | from_rule ctxt r = |
68 raise ERROR ("ThmC.from_rule: not defined for " ^ Rule.to_string_PIDE ctxt r); |
68 raise ERROR ("ThmC.from_rule: not defined for " ^ Rule.to_string ctxt r); |
69 |
69 |
70 \<^isac_test>\<open> |
70 \<^isac_test>\<open> |
71 fun string_of_thm_in_thy thy thm = |
71 fun string_of_thm_in_thy thy thm = |
72 UnparseC.term_in_ctxt (Proof_Context.init_global thy) (Thm.prop_of thm); |
72 UnparseC.term_in_ctxt (Proof_Context.init_global thy) (Thm.prop_of thm); |
73 \<close> |
73 \<close> |
149 "s" :: "y" :: "m" :: "_" :: id => implode id |
149 "s" :: "y" :: "m" :: "_" :: id => implode id |
150 | "#" :: ":" :: _ => "#: " ^ string_of_thm_PIDE ctxt thm' |
150 | "#" :: ":" :: _ => "#: " ^ string_of_thm_PIDE ctxt thm' |
151 | _ => "sym_" ^ thmID |
151 | _ => "sym_" ^ thmID |
152 in Rule.Thm (thmID', thm') end |
152 in Rule.Thm (thmID', thm') end |
153 | make_sym_rule _ (Rule.Rls_ rls) = Rule.Rls_ (make_sym_rule_set rls) |
153 | make_sym_rule _ (Rule.Rls_ rls) = Rule.Rls_ (make_sym_rule_set rls) |
154 | make_sym_rule ctxt r = raise ERROR ("ThmC.make_sym_rule: not for " ^ Rule.to_string_PIDE ctxt r) |
154 | make_sym_rule ctxt r = raise ERROR ("ThmC.make_sym_rule: not for " ^ Rule.to_string ctxt r) |
155 |
155 |
156 \<^isac_test>\<open> |
156 \<^isac_test>\<open> |
157 (* revert a thm RS @{thm sym} back to original thm, in case it ML\<open>is_sym\<close> *) |
157 (* revert a thm RS @{thm sym} back to original thm, in case it ML\<open>is_sym\<close> *) |
158 fun revert_sym_rule thy (Rule.Thm (id, thm)) = |
158 fun revert_sym_rule thy (Rule.Thm (id, thm)) = |
159 (*this ^^ might come from the user, who doesn't care about thy*) |
159 (*this ^^ might come from the user, who doesn't care about thy*) |
165 val id'' = Thm.get_name_hint thm' (*recover the thy the thm comes from*) |
165 val id'' = Thm.get_name_hint thm' (*recover the thy the thm comes from*) |
166 in Rule.Thm (id'', thm') end |
166 in Rule.Thm (id'', thm') end |
167 else Rule.Thm (Thm.get_name_hint thm, thm) (*recover the thy the thm comes from*) |
167 else Rule.Thm (Thm.get_name_hint thm, thm) (*recover the thy the thm comes from*) |
168 | revert_sym_rule thy rule = |
168 | revert_sym_rule thy rule = |
169 raise ERROR ("ThmC.revert_sym_rule: NOT for " ^ |
169 raise ERROR ("ThmC.revert_sym_rule: NOT for " ^ |
170 Rule.to_string_PIDE (Proof_Context.init_global thy) rule) |
170 Rule.to_string (Proof_Context.init_global thy) rule) |
171 \<close> |
171 \<close> |
172 |
172 |
173 |
173 |
174 (* ML antiquotations *) |
174 (* ML antiquotations *) |
175 |
175 |