isabelle: src/HOL/Library/SML_Quickcheck.thy@0460ff79bb52 (annotated)

33084 cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	1
cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	2	header {* Install quickcheck of SML code generator *}
cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	3
cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	4	theory SML_Quickcheck
cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	5	imports Main
cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	6	begin
cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	7
cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	8	setup {*
33771 17926df64f0f Added new counterexample generator SML_inductive for goals involving berghofe parents: 33084 diff changeset	9	InductiveCodegen.quickcheck_setup #>
33084 cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	10	Quickcheck.add_generator ("SML", Codegen.test_term)
cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	11	*}
cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	12
cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	13	end