equal
deleted
inserted
replaced
1064 \<close> |
1064 \<close> |
1065 |
1065 |
1066 (*<*)experiment begin(*>*) |
1066 (*<*)experiment begin(*>*) |
1067 attribute_setup my_rule = |
1067 attribute_setup my_rule = |
1068 \<open>Attrib.thms >> (fn ths => |
1068 \<open>Attrib.thms >> (fn ths => |
1069 Thm.rule_attribute |
1069 Thm.rule_attribute ths |
1070 (fn context: Context.generic => fn th: thm => |
1070 (fn context: Context.generic => fn th: thm => |
1071 let val th' = th OF ths |
1071 let val th' = th OF ths |
1072 in th' end))\<close> |
1072 in th' end))\<close> |
1073 |
1073 |
1074 attribute_setup my_declaration = |
1074 attribute_setup my_declaration = |