src/HOL/HOL.thy
changeset 57964 3dfc1bf3ac3d
parent 57963 cb67fac9bd89
child 58659 6c9821c32dd5
     1.1 --- a/src/HOL/HOL.thy	Sat Aug 16 21:11:08 2014 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat Aug 16 22:14:57 2014 +0200
     1.3 @@ -1921,35 +1921,14 @@
     1.4  
     1.5  subsubsection {* Nitpick setup *}
     1.6  
     1.7 -ML {*
     1.8 -structure Nitpick_Unfolds = Named_Thms
     1.9 -(
    1.10 -  val name = @{binding nitpick_unfold}
    1.11 -  val description = "alternative definitions of constants as needed by Nitpick"
    1.12 -)
    1.13 -structure Nitpick_Simps = Named_Thms
    1.14 -(
    1.15 -  val name = @{binding nitpick_simp}
    1.16 -  val description = "equational specification of constants as needed by Nitpick"
    1.17 -)
    1.18 -structure Nitpick_Psimps = Named_Thms
    1.19 -(
    1.20 -  val name = @{binding nitpick_psimp}
    1.21 -  val description = "partial equational specification of constants as needed by Nitpick"
    1.22 -)
    1.23 -structure Nitpick_Choice_Specs = Named_Thms
    1.24 -(
    1.25 -  val name = @{binding nitpick_choice_spec}
    1.26 -  val description = "choice specification of constants as needed by Nitpick"
    1.27 -)
    1.28 -*}
    1.29 -
    1.30 -setup {*
    1.31 -  Nitpick_Unfolds.setup
    1.32 -  #> Nitpick_Simps.setup
    1.33 -  #> Nitpick_Psimps.setup
    1.34 -  #> Nitpick_Choice_Specs.setup
    1.35 -*}
    1.36 +named_theorems nitpick_unfold
    1.37 +  "alternative definitions of constants as needed by Nitpick"
    1.38 +named_theorems nitpick_simp
    1.39 +  "equational specification of constants as needed by Nitpick"
    1.40 +named_theorems nitpick_psimp
    1.41 +  "partial equational specification of constants as needed by Nitpick"
    1.42 +named_theorems nitpick_choice_spec
    1.43 +  "choice specification of constants as needed by Nitpick"
    1.44  
    1.45  declare if_bool_eq_conj [nitpick_unfold, no_atp]
    1.46          if_bool_eq_disj [no_atp]