# HG changeset patch
# User wenzelm
# Date 1416652560 -3600
# Node ID df7476e7955808b02f2829ffbf484e417442580f
# Parent  f9bee88c59129c73e715039ea6c99e26c96e3ccb
named_theorems: multiple args;

diff -r f9bee88c5912 -r df7476e79558 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Fri Nov 21 22:59:32 2014 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Sat Nov 22 11:36:00 2014 +0100
@@ -1394,7 +1394,7 @@
       (@'for' (@{syntax vars} + @'and'))?
     ;
     @@{command named_theorems} @{syntax target}?
-      @{syntax name} @{syntax text}?
+      (@{syntax name} @{syntax text}? + @'and')
   \<close>}
 
   \begin{description}
diff -r f9bee88c5912 -r df7476e79558 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Nov 21 22:59:32 2014 +0100
+++ b/src/HOL/HOL.thy	Sat Nov 22 11:36:00 2014 +0100
@@ -1948,14 +1948,10 @@
 
 subsubsection {* Nitpick setup *}
 
-named_theorems nitpick_unfold
-  "alternative definitions of constants as needed by Nitpick"
-named_theorems nitpick_simp
-  "equational specification of constants as needed by Nitpick"
-named_theorems nitpick_psimp
-  "partial equational specification of constants as needed by Nitpick"
-named_theorems nitpick_choice_spec
-  "choice specification of constants as needed by Nitpick"
+named_theorems nitpick_unfold "alternative definitions of constants as needed by Nitpick"
+  and nitpick_simp "equational specification of constants as needed by Nitpick"
+  and nitpick_psimp "partial equational specification of constants as needed by Nitpick"
+  and nitpick_choice_spec "choice specification of constants as needed by Nitpick"
 
 declare if_bool_eq_conj [nitpick_unfold, no_atp]
         if_bool_eq_disj [no_atp]
@@ -1963,12 +1959,9 @@
 
 subsection {* Preprocessing for the predicate compiler *}
 
-named_theorems code_pred_def
-  "alternative definitions of constants for the Predicate Compiler"
-named_theorems code_pred_inline
-  "inlining definitions for the Predicate Compiler"
-named_theorems code_pred_simp
-  "simplification rules for the optimisations in the Predicate Compiler"
+named_theorems code_pred_def "alternative definitions of constants for the Predicate Compiler"
+  and code_pred_inline "inlining definitions for the Predicate Compiler"
+  and code_pred_simp "simplification rules for the optimisations in the Predicate Compiler"
 
 
 subsection {* Legacy tactics and ML bindings *}
diff -r f9bee88c5912 -r df7476e79558 src/HOL/HOLCF/Domain.thy
--- a/src/HOL/HOLCF/Domain.thy	Fri Nov 21 22:59:32 2014 +0100
+++ b/src/HOL/HOLCF/Domain.thy	Sat Nov 22 11:36:00 2014 +0100
@@ -317,7 +317,7 @@
 subsection {* Setting up the domain package *}
 
 named_theorems domain_defl_simps "theorems like DEFL('a t) = t_defl$DEFL('a)"
-named_theorems domain_isodefl "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
+  and domain_isodefl "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
 
 ML_file "Tools/Domain/domain_isomorphism.ML"
 ML_file "Tools/Domain/domain_axioms.ML"
diff -r f9bee88c5912 -r df7476e79558 src/HOL/HOLCF/Domain_Aux.thy
--- a/src/HOL/HOLCF/Domain_Aux.thy	Fri Nov 21 22:59:32 2014 +0100
+++ b/src/HOL/HOLCF/Domain_Aux.thy	Sat Nov 22 11:36:00 2014 +0100
@@ -345,7 +345,7 @@
 subsection {* ML setup *}
 
 named_theorems domain_deflation "theorems like deflation a ==> deflation (foo_map$a)"
-named_theorems domain_map_ID "theorems like foo_map$ID = ID"
+  and domain_map_ID "theorems like foo_map$ID = ID"
 
 ML_file "Tools/Domain/domain_take_proofs.ML"
 ML_file "Tools/cont_consts.ML"
diff -r f9bee88c5912 -r df7476e79558 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Nov 21 22:59:32 2014 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Sat Nov 22 11:36:00 2014 +0100
@@ -154,7 +154,7 @@
   using assms unfolding effect_def by auto
 
 named_theorems effect_intros "introduction rules for effect"
-named_theorems effect_elims "elimination rules for effect"
+  and effect_elims "elimination rules for effect"
 
 lemma effect_LetI [effect_intros]:
   assumes "x = t" "effect (f x) h h' r"
diff -r f9bee88c5912 -r df7476e79558 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Fri Nov 21 22:59:32 2014 +0100
+++ b/src/HOL/Quotient.thy	Sat Nov 22 11:36:00 2014 +0100
@@ -749,10 +749,10 @@
 text {* Auxiliary data for the quotient package *}
 
 named_theorems quot_equiv "equivalence relation theorems"
-named_theorems quot_respect "respectfulness theorems"
-named_theorems quot_preserve "preservation theorems"
-named_theorems id_simps "identity simp rules for maps"
-named_theorems quot_thm "quotient theorems"
+  and quot_respect "respectfulness theorems"
+  and quot_preserve "preservation theorems"
+  and id_simps "identity simp rules for maps"
+  and quot_thm "quotient theorems"
 ML_file "Tools/Quotient/quotient_info.ML"
 
 declare [[mapQ3 "fun" = (rel_fun, fun_quotient3)]]
diff -r f9bee88c5912 -r df7476e79558 src/Pure/Tools/named_theorems.ML
--- a/src/Pure/Tools/named_theorems.ML	Fri Nov 21 22:59:32 2014 +0100
+++ b/src/Pure/Tools/named_theorems.ML	Sat Nov 22 11:36:00 2014 +0100
@@ -74,7 +74,8 @@
 val _ =
   Outer_Syntax.local_theory @{command_spec "named_theorems"}
     "declare named collection of theorems"
-    (Parse.binding -- Scan.optional Parse.text "" >> (fn (b, descr) => snd o declare b descr));
+    (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
+      fold (fn (b, descr) => snd o declare b descr));
 
 
 (* ML antiquotation *)