equal
deleted
inserted
replaced
90 end |
90 end |
91 \<close> |
91 \<close> |
92 |
92 |
93 ML \<open> |
93 ML \<open> |
94 val _ = Outer_Syntax.local_theory' \<^command_keyword>\<open>lemmas_with\<close> "note theorems with (the same) attributes" |
94 val _ = Outer_Syntax.local_theory' \<^command_keyword>\<open>lemmas_with\<close> "note theorems with (the same) attributes" |
95 (Parse.attribs --| @{keyword :} -- Parse_Spec.name_facts -- Parse.for_fixes |
95 (Parse.attribs --| \<^keyword>\<open>:\<close> -- Parse_Spec.name_facts -- Parse.for_fixes |
96 >> (fn (((attrs),facts), fixes) => |
96 >> (fn (((attrs),facts), fixes) => |
97 #2 oo Specification.theorems_cmd Thm.theoremK |
97 #2 oo Specification.theorems_cmd Thm.theoremK |
98 (map (apsnd (map (apsnd (fn xs => attrs@xs)))) facts) fixes)) |
98 (map (apsnd (map (apsnd (fn xs => attrs@xs)))) facts) fixes)) |
99 \<close> |
99 \<close> |
100 |
100 |