author | nipkow |
Tue, 21 Dec 2010 08:38:03 +0100 | |
changeset 41341 | e65a122057ad |
parent 39252 | 8f176e575a49 |
child 43886 | bf068e758783 |
permissions | -rw-r--r-- |
35953 | 1 |
(* Author: Lukas Bulwahn, TU Muenchen *) |
2 |
||
3 |
header {* A Prototype of Quickcheck based on the Predicate Compiler *} |
|
4 |
||
5 |
theory Predicate_Compile_Quickcheck |
|
6 |
imports Main Predicate_Compile_Alternative_Defs |
|
7 |
uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML" |
|
8 |
begin |
|
9 |
||
39252
8f176e575a49
changing the container for the quickcheck options to a generic data
bulwahn
parents:
36026
diff
changeset
|
10 |
setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term |
8f176e575a49
changing the container for the quickcheck options to a generic data
bulwahn
parents:
36026
diff
changeset
|
11 |
Predicate_Compile_Aux.New_Pos_Random_DSeq false true 4)) *} |
8f176e575a49
changing the container for the quickcheck options to a generic data
bulwahn
parents:
36026
diff
changeset
|
12 |
setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_ff_fs", |
8f176e575a49
changing the container for the quickcheck options to a generic data
bulwahn
parents:
36026
diff
changeset
|
13 |
Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true true 4)) *} |
8f176e575a49
changing the container for the quickcheck options to a generic data
bulwahn
parents:
36026
diff
changeset
|
14 |
setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_ff_nofs", |
8f176e575a49
changing the container for the quickcheck options to a generic data
bulwahn
parents:
36026
diff
changeset
|
15 |
Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true false 4)) *} |
35953 | 16 |
|
17 |
end |