src/HOL/Quickcheck_Examples/ROOT.ML
author bulwahn
Sat, 21 Jul 2012 10:55:42 +0200
changeset 48415 b42067a3188f
parent 48356 b6081af563a9
child 48596 3defa60a7ae3
permissions -rw-r--r--
restricting Quickcheck_Examples' root file to one basic theory to see if the system error on isatest still occurs

use_thys [
(*  "Find_Unused_Assms_Examples", *)
  "Quickcheck_Examples"
  (*,
  "Quickcheck_Lattice_Examples",
  "Completeness",
  "Quickcheck_Interfaces",
  "Hotel_Example",
  "Needham_Schroeder_No_Attacker_Example",
  "Needham_Schroeder_Guided_Attacker_Example",
  "Needham_Schroeder_Unguided_Attacker_Example"*)
];
(*
if getenv "ISABELLE_GHC" = "" then ()
else use_thy "Quickcheck_Narrowing_Examples";
*)