summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sat, 22 Nov 2014 11:36:00 +0100 | |

changeset 59028 | df7476e79558 |

parent 59027 | f9bee88c5912 |

child 59029 | c907cbe36713 |

named_theorems: multiple args;

--- 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 *)