named_theorems: multiple args;
authorwenzelm
Sat Nov 22 11:36:00 2014 +0100 (2014-11-22)
changeset 59028df7476e79558
parent 59027 f9bee88c5912
child 59029 c907cbe36713
named_theorems: multiple args;
src/Doc/Isar_Ref/Spec.thy
src/HOL/HOL.thy
src/HOL/HOLCF/Domain.thy
src/HOL/HOLCF/Domain_Aux.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Quotient.thy
src/Pure/Tools/named_theorems.ML
     1.1 --- a/src/Doc/Isar_Ref/Spec.thy	Fri Nov 21 22:59:32 2014 +0100
     1.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Sat Nov 22 11:36:00 2014 +0100
     1.3 @@ -1394,7 +1394,7 @@
     1.4        (@'for' (@{syntax vars} + @'and'))?
     1.5      ;
     1.6      @@{command named_theorems} @{syntax target}?
     1.7 -      @{syntax name} @{syntax text}?
     1.8 +      (@{syntax name} @{syntax text}? + @'and')
     1.9    \<close>}
    1.10  
    1.11    \begin{description}
     2.1 --- a/src/HOL/HOL.thy	Fri Nov 21 22:59:32 2014 +0100
     2.2 +++ b/src/HOL/HOL.thy	Sat Nov 22 11:36:00 2014 +0100
     2.3 @@ -1948,14 +1948,10 @@
     2.4  
     2.5  subsubsection {* Nitpick setup *}
     2.6  
     2.7 -named_theorems nitpick_unfold
     2.8 -  "alternative definitions of constants as needed by Nitpick"
     2.9 -named_theorems nitpick_simp
    2.10 -  "equational specification of constants as needed by Nitpick"
    2.11 -named_theorems nitpick_psimp
    2.12 -  "partial equational specification of constants as needed by Nitpick"
    2.13 -named_theorems nitpick_choice_spec
    2.14 -  "choice specification of constants as needed by Nitpick"
    2.15 +named_theorems nitpick_unfold "alternative definitions of constants as needed by Nitpick"
    2.16 +  and nitpick_simp "equational specification of constants as needed by Nitpick"
    2.17 +  and nitpick_psimp "partial equational specification of constants as needed by Nitpick"
    2.18 +  and nitpick_choice_spec "choice specification of constants as needed by Nitpick"
    2.19  
    2.20  declare if_bool_eq_conj [nitpick_unfold, no_atp]
    2.21          if_bool_eq_disj [no_atp]
    2.22 @@ -1963,12 +1959,9 @@
    2.23  
    2.24  subsection {* Preprocessing for the predicate compiler *}
    2.25  
    2.26 -named_theorems code_pred_def
    2.27 -  "alternative definitions of constants for the Predicate Compiler"
    2.28 -named_theorems code_pred_inline
    2.29 -  "inlining definitions for the Predicate Compiler"
    2.30 -named_theorems code_pred_simp
    2.31 -  "simplification rules for the optimisations in the Predicate Compiler"
    2.32 +named_theorems code_pred_def "alternative definitions of constants for the Predicate Compiler"
    2.33 +  and code_pred_inline "inlining definitions for the Predicate Compiler"
    2.34 +  and code_pred_simp "simplification rules for the optimisations in the Predicate Compiler"
    2.35  
    2.36  
    2.37  subsection {* Legacy tactics and ML bindings *}
     3.1 --- a/src/HOL/HOLCF/Domain.thy	Fri Nov 21 22:59:32 2014 +0100
     3.2 +++ b/src/HOL/HOLCF/Domain.thy	Sat Nov 22 11:36:00 2014 +0100
     3.3 @@ -317,7 +317,7 @@
     3.4  subsection {* Setting up the domain package *}
     3.5  
     3.6  named_theorems domain_defl_simps "theorems like DEFL('a t) = t_defl$DEFL('a)"
     3.7 -named_theorems domain_isodefl "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
     3.8 +  and domain_isodefl "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
     3.9  
    3.10  ML_file "Tools/Domain/domain_isomorphism.ML"
    3.11  ML_file "Tools/Domain/domain_axioms.ML"
     4.1 --- a/src/HOL/HOLCF/Domain_Aux.thy	Fri Nov 21 22:59:32 2014 +0100
     4.2 +++ b/src/HOL/HOLCF/Domain_Aux.thy	Sat Nov 22 11:36:00 2014 +0100
     4.3 @@ -345,7 +345,7 @@
     4.4  subsection {* ML setup *}
     4.5  
     4.6  named_theorems domain_deflation "theorems like deflation a ==> deflation (foo_map$a)"
     4.7 -named_theorems domain_map_ID "theorems like foo_map$ID = ID"
     4.8 +  and domain_map_ID "theorems like foo_map$ID = ID"
     4.9  
    4.10  ML_file "Tools/Domain/domain_take_proofs.ML"
    4.11  ML_file "Tools/cont_consts.ML"
     5.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Nov 21 22:59:32 2014 +0100
     5.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Sat Nov 22 11:36:00 2014 +0100
     5.3 @@ -154,7 +154,7 @@
     5.4    using assms unfolding effect_def by auto
     5.5  
     5.6  named_theorems effect_intros "introduction rules for effect"
     5.7 -named_theorems effect_elims "elimination rules for effect"
     5.8 +  and effect_elims "elimination rules for effect"
     5.9  
    5.10  lemma effect_LetI [effect_intros]:
    5.11    assumes "x = t" "effect (f x) h h' r"
     6.1 --- a/src/HOL/Quotient.thy	Fri Nov 21 22:59:32 2014 +0100
     6.2 +++ b/src/HOL/Quotient.thy	Sat Nov 22 11:36:00 2014 +0100
     6.3 @@ -749,10 +749,10 @@
     6.4  text {* Auxiliary data for the quotient package *}
     6.5  
     6.6  named_theorems quot_equiv "equivalence relation theorems"
     6.7 -named_theorems quot_respect "respectfulness theorems"
     6.8 -named_theorems quot_preserve "preservation theorems"
     6.9 -named_theorems id_simps "identity simp rules for maps"
    6.10 -named_theorems quot_thm "quotient theorems"
    6.11 +  and quot_respect "respectfulness theorems"
    6.12 +  and quot_preserve "preservation theorems"
    6.13 +  and id_simps "identity simp rules for maps"
    6.14 +  and quot_thm "quotient theorems"
    6.15  ML_file "Tools/Quotient/quotient_info.ML"
    6.16  
    6.17  declare [[mapQ3 "fun" = (rel_fun, fun_quotient3)]]
     7.1 --- a/src/Pure/Tools/named_theorems.ML	Fri Nov 21 22:59:32 2014 +0100
     7.2 +++ b/src/Pure/Tools/named_theorems.ML	Sat Nov 22 11:36:00 2014 +0100
     7.3 @@ -74,7 +74,8 @@
     7.4  val _ =
     7.5    Outer_Syntax.local_theory @{command_spec "named_theorems"}
     7.6      "declare named collection of theorems"
     7.7 -    (Parse.binding -- Scan.optional Parse.text "" >> (fn (b, descr) => snd o declare b descr));
     7.8 +    (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
     7.9 +      fold (fn (b, descr) => snd o declare b descr));
    7.10  
    7.11  
    7.12  (* ML antiquotation *)