added predicate compile preprocessing structure for definitional thms -- probably is replaced by hooking the theorem command differently
authorbulwahn
Wed Sep 23 16:20:12 2009 +0200 (2009-09-23)
changeset 32660e3aab585531d
parent 32659 ffe062d9ae95
child 32661 f4d179d91af2
added predicate compile preprocessing structure for definitional thms -- probably is replaced by hooking the theorem command differently
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Wed Sep 23 16:20:12 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Sep 23 16:20:12 2009 +0200
     1.3 @@ -2021,6 +2021,15 @@
     1.4  
     1.5  quickcheck_params [size = 5, iterations = 50]
     1.6  
     1.7 +subsection {* Preprocessing for the predicate compiler *}
     1.8 +
     1.9 +ML {*
    1.10 +structure Predicate_Compile_Preproc_Const_Defs = Named_Thms
    1.11 +(
    1.12 +  val name = "predicate_compile_preproc_const_def"
    1.13 +  val description = "definitions of constants as needed by the preprocessing for the predicate compiler "
    1.14 +)
    1.15 +*}
    1.16  
    1.17  subsection {* Nitpick setup *}
    1.18