src/HOL/Quickcheck_Examples/ROOT.ML
changeset 48415 b42067a3188f
parent 48356 b6081af563a9
child 48596 3defa60a7ae3
equal deleted inserted replaced
48414:43875bab3a4c 48415:b42067a3188f
     1 use_thys [
     1 use_thys [
     2 (*  "Find_Unused_Assms_Examples", *)
     2 (*  "Find_Unused_Assms_Examples", *)
     3   "Quickcheck_Examples",
     3   "Quickcheck_Examples"
       
     4   (*,
     4   "Quickcheck_Lattice_Examples",
     5   "Quickcheck_Lattice_Examples",
     5   "Completeness",
     6   "Completeness",
     6   "Quickcheck_Interfaces",
     7   "Quickcheck_Interfaces",
     7   "Hotel_Example",
     8   "Hotel_Example",
     8   "Needham_Schroeder_No_Attacker_Example",
     9   "Needham_Schroeder_No_Attacker_Example",
     9   "Needham_Schroeder_Guided_Attacker_Example",
    10   "Needham_Schroeder_Guided_Attacker_Example",
    10   "Needham_Schroeder_Unguided_Attacker_Example"
    11   "Needham_Schroeder_Unguided_Attacker_Example"*)
    11 ];
    12 ];
    12 (*
    13 (*
    13 if getenv "ISABELLE_GHC" = "" then ()
    14 if getenv "ISABELLE_GHC" = "" then ()
    14 else use_thy "Quickcheck_Narrowing_Examples";
    15 else use_thy "Quickcheck_Narrowing_Examples";
    15 *)
    16 *)