Theory CZH_Utilities

(* Copyright 2021 (C) Mihails Milehins *)

section‹Utilities›
theory CZH_Utilities
  imports Main
  keywords "lemmas_with" :: thy_decl
begin


text‹
Then command \<^text>‹lemmas_with› is a copy (with minor amendments to formatting) 
of the command with the identical name that was introduced by Ondřej Kunčar in
\<^text>‹HOL-Types_To_Sets.Prerequisites›. A copy of the function was produced, 
primarily, to avoid the unnecessary dependency of this work on the 
axioms associated with the framework ‹Types-To-Sets›.
›

ML‹
val _ =
  Outer_Syntax.local_theory'
    \<^command_keyword>‹lemmas_with› 
    "note theorems with (the same) attributes"
    (
      Parse.attribs --| \<^keyword>‹:› --
      Parse_Spec.name_facts -- 
      Parse.for_fixes >> 
      (
        fn (((attrs),facts), fixes) =>
          #2 oo Specification.theorems_cmd Thm.theoremK
          (map (apsnd (map (apsnd (fn xs => attrs@xs)))) facts) fixes
      )
    )
›

text‹\newpage›

end