equal
deleted
inserted
replaced
60 Global_Theory.add_thms_dynamic |
60 Global_Theory.add_thms_dynamic |
61 (\<^binding>\<open>derivative_eq_intros\<close>, |
61 (\<^binding>\<open>derivative_eq_intros\<close>, |
62 fn context => |
62 fn context => |
63 Named_Theorems.get (Context.proof_of context) @{named_theorems derivative_intros} |
63 Named_Theorems.get (Context.proof_of context) @{named_theorems derivative_intros} |
64 |> map_filter eq_rule) |
64 |> map_filter eq_rule) |
65 end; |
65 end |
66 \<close> |
66 \<close> |
67 |
67 |
68 text \<open> |
68 text \<open> |
69 The following syntax is only used as a legacy syntax. |
69 The following syntax is only used as a legacy syntax. |
70 \<close> |
70 \<close> |