src/HOL/Quickcheck_Examples/ROOT.ML

deactivate Find_Unused_Assms_Examples to see if isabelle test's failures is caused by this example file

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