more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
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