# HG changeset patch
# User bulwahn
# Date 1253715612 -7200
# Node ID e3aab585531da5fbae165463e370c505895dfc16
# Parent  ffe062d9ae95cdfe7dc8309a6402144eaef6bc46
added predicate compile preprocessing structure for definitional thms -- probably is replaced by hooking the theorem command differently

diff -r ffe062d9ae95 -r e3aab585531d src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/HOL.thy	Wed Sep 23 16:20:12 2009 +0200
@@ -2021,6 +2021,15 @@
 
 quickcheck_params [size = 5, iterations = 50]
 
+subsection {* Preprocessing for the predicate compiler *}
+
+ML {*
+structure Predicate_Compile_Preproc_Const_Defs = Named_Thms
+(
+  val name = "predicate_compile_preproc_const_def"
+  val description = "definitions of constants as needed by the preprocessing for the predicate compiler "
+)
+*}
 
 subsection {* Nitpick setup *}