--- 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}
--- 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 *}
--- 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"
--- 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"
--- 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"
--- 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)]]
--- 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 *)