src/HOL/HOL.thy
changeset 45294 3c5d3d286055
parent 45231 d85a2fdc586c
child 45607 16b4f5774621
     1.1 --- a/src/HOL/HOL.thy	Fri Oct 28 23:16:50 2011 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Oct 28 23:41:16 2011 +0200
     1.3 @@ -805,7 +805,7 @@
     1.4  ML {*
     1.5  structure No_ATPs = Named_Thms
     1.6  (
     1.7 -  val name = "no_atp"
     1.8 +  val name = @{binding no_atp}
     1.9    val description = "theorems that should be filtered out by Sledgehammer"
    1.10  )
    1.11  *}
    1.12 @@ -1937,22 +1937,22 @@
    1.13  ML {*
    1.14  structure Nitpick_Unfolds = Named_Thms
    1.15  (
    1.16 -  val name = "nitpick_unfold"
    1.17 +  val name = @{binding nitpick_unfold}
    1.18    val description = "alternative definitions of constants as needed by Nitpick"
    1.19  )
    1.20  structure Nitpick_Simps = Named_Thms
    1.21  (
    1.22 -  val name = "nitpick_simp"
    1.23 +  val name = @{binding nitpick_simp}
    1.24    val description = "equational specification of constants as needed by Nitpick"
    1.25  )
    1.26  structure Nitpick_Psimps = Named_Thms
    1.27  (
    1.28 -  val name = "nitpick_psimp"
    1.29 +  val name = @{binding nitpick_psimp}
    1.30    val description = "partial equational specification of constants as needed by Nitpick"
    1.31  )
    1.32  structure Nitpick_Choice_Specs = Named_Thms
    1.33  (
    1.34 -  val name = "nitpick_choice_spec"
    1.35 +  val name = @{binding nitpick_choice_spec}
    1.36    val description = "choice specification of constants as needed by Nitpick"
    1.37  )
    1.38  *}
    1.39 @@ -1973,17 +1973,17 @@
    1.40  ML {*
    1.41  structure Predicate_Compile_Alternative_Defs = Named_Thms
    1.42  (
    1.43 -  val name = "code_pred_def"
    1.44 +  val name = @{binding code_pred_def}
    1.45    val description = "alternative definitions of constants for the Predicate Compiler"
    1.46  )
    1.47  structure Predicate_Compile_Inline_Defs = Named_Thms
    1.48  (
    1.49 -  val name = "code_pred_inline"
    1.50 +  val name = @{binding code_pred_inline}
    1.51    val description = "inlining definitions for the Predicate Compiler"
    1.52  )
    1.53  structure Predicate_Compile_Simps = Named_Thms
    1.54  (
    1.55 -  val name = "code_pred_simp"
    1.56 +  val name = @{binding code_pred_simp}
    1.57    val description = "simplification rules for the optimisations in the Predicate Compiler"
    1.58  )
    1.59  *}