src/HOL/Library/Predicate_Compile_Quickcheck.thy
changeset 35953 0460ff79bb52
child 36026 276ebec72082
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Wed Mar 24 17:40:43 2010 +0100
     1.3 @@ -0,0 +1,14 @@
     1.4 +(* Author: Lukas Bulwahn, TU Muenchen *)
     1.5 +
     1.6 +header {* A Prototype of Quickcheck based on the Predicate Compiler *}
     1.7 +
     1.8 +theory Predicate_Compile_Quickcheck
     1.9 +imports Main Predicate_Compile_Alternative_Defs
    1.10 +uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
    1.11 +begin
    1.12 +
    1.13 +setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term false true 4) *}
    1.14 +setup {* Quickcheck.add_generator ("predicate_compile_ff_fs", Predicate_Compile_Quickcheck.quickcheck_compile_term true true 4) *}
    1.15 +setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs", Predicate_Compile_Quickcheck.quickcheck_compile_term true false 4) *}
    1.16 +
    1.17 +end
    1.18 \ No newline at end of file