src/HOL/HOL.thy
changeset 59028 df7476e79558
parent 58963 26bf09b95dda
child 59498 50b60f501b05
child 59504 8c6747dba731
     1.1 --- a/src/HOL/HOL.thy	Fri Nov 21 22:59:32 2014 +0100
     1.2 +++ b/src/HOL/HOL.thy	Sat Nov 22 11:36:00 2014 +0100
     1.3 @@ -1948,14 +1948,10 @@
     1.4  
     1.5  subsubsection {* Nitpick setup *}
     1.6  
     1.7 -named_theorems nitpick_unfold
     1.8 -  "alternative definitions of constants as needed by Nitpick"
     1.9 -named_theorems nitpick_simp
    1.10 -  "equational specification of constants as needed by Nitpick"
    1.11 -named_theorems nitpick_psimp
    1.12 -  "partial equational specification of constants as needed by Nitpick"
    1.13 -named_theorems nitpick_choice_spec
    1.14 -  "choice specification of constants as needed by Nitpick"
    1.15 +named_theorems nitpick_unfold "alternative definitions of constants as needed by Nitpick"
    1.16 +  and nitpick_simp "equational specification of constants as needed by Nitpick"
    1.17 +  and nitpick_psimp "partial equational specification of constants as needed by Nitpick"
    1.18 +  and nitpick_choice_spec "choice specification of constants as needed by Nitpick"
    1.19  
    1.20  declare if_bool_eq_conj [nitpick_unfold, no_atp]
    1.21          if_bool_eq_disj [no_atp]
    1.22 @@ -1963,12 +1959,9 @@
    1.23  
    1.24  subsection {* Preprocessing for the predicate compiler *}
    1.25  
    1.26 -named_theorems code_pred_def
    1.27 -  "alternative definitions of constants for the Predicate Compiler"
    1.28 -named_theorems code_pred_inline
    1.29 -  "inlining definitions for the Predicate Compiler"
    1.30 -named_theorems code_pred_simp
    1.31 -  "simplification rules for the optimisations in the Predicate Compiler"
    1.32 +named_theorems code_pred_def "alternative definitions of constants for the Predicate Compiler"
    1.33 +  and code_pred_inline "inlining definitions for the Predicate Compiler"
    1.34 +  and code_pred_simp "simplification rules for the optimisations in the Predicate Compiler"
    1.35  
    1.36  
    1.37  subsection {* Legacy tactics and ML bindings *}