changeset 46950 | d0181abdbdac |
parent 46664 | 1f6c140f9c72 |
child 48891 | c0eafbd55de3 |
--- a/src/HOL/Predicate_Compile.thy Thu Mar 15 20:07:00 2012 +0100 +++ b/src/HOL/Predicate_Compile.thy Thu Mar 15 22:08:53 2012 +0100 @@ -6,6 +6,7 @@ theory Predicate_Compile imports Predicate New_Random_Sequence Quickcheck_Exhaustive +keywords "code_pred" :: thy_goal and "values" :: diag uses "Tools/Predicate_Compile/predicate_compile_aux.ML" "Tools/Predicate_Compile/predicate_compile_compilations.ML"