src/HOL/Quickcheck_Examples/ROOT.ML
author bulwahn
Fri, 30 Mar 2012 08:44:01 +0200
changeset 47205 34e8b7347dda
parent 46701 879f5c76ffb6
child 48179 18461f745b4a
permissions -rw-r--r--
adding theory to prove completeness of the exhaustive generators

use_thys [
  "Find_Unused_Assms_Examples",
  "Quickcheck_Examples",
  "Quickcheck_Lattice_Examples",
  "Completeness"
];

if getenv "ISABELLE_GHC" = "" then ()
else use_thy "Quickcheck_Narrowing_Examples";