src/HOL/Library/SML_Quickcheck.thy

do proofs using Rep_Sprod_simps, Rep_Ssum_simps; remove unused lemmas

header {* Install quickcheck of SML code generator *}

theory SML_Quickcheck
imports Main
begin

setup {*
  Inductive_Codegen.quickcheck_setup #>
  Context.theory_map (Quickcheck.add_generator ("SML", Codegen.test_term))
*}

end