author | haftmann |
Thu, 18 Nov 2010 17:01:16 +0100 | |
changeset 40606 | af1a0b0c6202 |
parent 39252 | 8f176e575a49 |
child 40919 | cdb34f393a7e |
permissions | -rw-r--r-- |
33084 | 1 |
|
2 |
header {* Install quickcheck of SML code generator *} |
|
3 |
||
4 |
theory SML_Quickcheck |
|
5 |
imports Main |
|
6 |
begin |
|
7 |
||
8 |
setup {* |
|
37390
8781d80026fc
moved inductive_codegen to place where product type is available; tuned structure name
haftmann
parents:
33771
diff
changeset
|
9 |
Inductive_Codegen.quickcheck_setup #> |
39252
8f176e575a49
changing the container for the quickcheck options to a generic data
bulwahn
parents:
37390
diff
changeset
|
10 |
Context.theory_map (Quickcheck.add_generator ("SML", Codegen.test_term)) |
33084 | 11 |
*} |
12 |
||
13 |
end |