changeset 36176 | 3fe7e97ccca8 |
parent 36040 | fcd7bea01a93 |
child 39191 | edaf5a6ffa99 |
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Fri Apr 16 20:56:40 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Fri Apr 16 21:28:09 2010 +0200 @@ -150,7 +150,7 @@ quickcheck[generator = predicate_compile_ff_nofs, size=5, iterations=1] oops -hide const a b +hide_const a b subsection {* Lexicographic order *} (* TODO *)