src/HOL/Quickcheck_Examples/ROOT.ML
author bulwahn
Thu, 19 Jul 2012 12:01:05 +0200
changeset 48356 b6081af563a9
parent 48267 f5676fad35a3
child 48415 b42067a3188f
permissions -rw-r--r--
deactivating quickcheck narrowing examples to find out if this causes the system error on the current isatest

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";
*)