adding some basic handling that unfolds a conjecture in a locale before testing it with quickcheck
(* Title: CTT/ex/ROOT.ML
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Examples for Constructive Type Theory.
*)
use_thys ["Typechecking", "Elimination", "Equality", "Synthesis"];