src/HOL/Library/SML_Quickcheck.thy
author haftmann
Thu Jun 10 12:24:02 2010 +0200 (2010-06-10)
changeset 37390 8781d80026fc
parent 33771 17926df64f0f
child 39252 8f176e575a49
permissions -rw-r--r--
moved inductive_codegen to place where product type is available; tuned structure name
haftmann@33084
     1
haftmann@33084
     2
header {* Install quickcheck of SML code generator *}
haftmann@33084
     3
haftmann@33084
     4
theory SML_Quickcheck
haftmann@33084
     5
imports Main
haftmann@33084
     6
begin
haftmann@33084
     7
haftmann@33084
     8
setup {*
haftmann@37390
     9
  Inductive_Codegen.quickcheck_setup #>
haftmann@33084
    10
  Quickcheck.add_generator ("SML", Codegen.test_term)
haftmann@33084
    11
*}
haftmann@33084
    12
haftmann@33084
    13
end