src/HOL/Quickcheck_Examples/ROOT.ML
changeset 48356 b6081af563a9
parent 48267 f5676fad35a3
child 48415 b42067a3188f
equal deleted inserted replaced
48343:3060e6343953 48356:b6081af563a9
     7   "Hotel_Example",
     7   "Hotel_Example",
     8   "Needham_Schroeder_No_Attacker_Example",
     8   "Needham_Schroeder_No_Attacker_Example",
     9   "Needham_Schroeder_Guided_Attacker_Example",
     9   "Needham_Schroeder_Guided_Attacker_Example",
    10   "Needham_Schroeder_Unguided_Attacker_Example"
    10   "Needham_Schroeder_Unguided_Attacker_Example"
    11 ];
    11 ];
    12 
    12 (*
    13 if getenv "ISABELLE_GHC" = "" then ()
    13 if getenv "ISABELLE_GHC" = "" then ()
    14 else use_thy "Quickcheck_Narrowing_Examples";
    14 else use_thy "Quickcheck_Narrowing_Examples";
    15 
    15 *)