src/HOL/Library/SML_Quickcheck.thy
author wenzelm
Wed, 04 Aug 2010 16:11:51 +0200
changeset 38147 2b08a96a283e
parent 37390 8781d80026fc
child 39252 8f176e575a49
permissions -rw-r--r--
load_thy/after_load: explicit check of parent theories, which might have failed to join proofs -- avoid uninformative crash via Graph.UNDEF;


header {* Install quickcheck of SML code generator *}

theory SML_Quickcheck
imports Main
begin

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

end