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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46585
f462e49eaf11 moving Quickcheck's example to its own session
bulwahn
parents:
diff changeset
     1
use_thys [
48267
f5676fad35a3 deactivate Find_Unused_Assms_Examples to see if isabelle test's failures is caused by this example file
bulwahn
parents: 48243
diff changeset
     2
(*  "Find_Unused_Assms_Examples", *)
46585
f462e49eaf11 moving Quickcheck's example to its own session
bulwahn
parents:
diff changeset
     3
  "Quickcheck_Examples",
47205
34e8b7347dda adding theory to prove completeness of the exhaustive generators
bulwahn
parents: 46701
diff changeset
     4
  "Quickcheck_Lattice_Examples",
48179
18461f745b4a adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents: 47205
diff changeset
     5
  "Completeness",
48222
fcca68383808 adding the hotel key card example in Quickcheck-Examples
bulwahn
parents: 48179
diff changeset
     6
  "Quickcheck_Interfaces",
48224
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents: 48222
diff changeset
     7
  "Hotel_Example",
48243
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents: 48224
diff changeset
     8
  "Needham_Schroeder_No_Attacker_Example",
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents: 48224
diff changeset
     9
  "Needham_Schroeder_Guided_Attacker_Example",
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents: 48224
diff changeset
    10
  "Needham_Schroeder_Unguided_Attacker_Example"
46585
f462e49eaf11 moving Quickcheck's example to its own session
bulwahn
parents:
diff changeset
    11
];
48356
b6081af563a9 deactivating quickcheck narrowing examples to find out if this causes the system error on the current isatest
bulwahn
parents: 48267
diff changeset
    12
(*
46585
f462e49eaf11 moving Quickcheck's example to its own session
bulwahn
parents:
diff changeset
    13
if getenv "ISABELLE_GHC" = "" then ()
f462e49eaf11 moving Quickcheck's example to its own session
bulwahn
parents:
diff changeset
    14
else use_thy "Quickcheck_Narrowing_Examples";
48356
b6081af563a9 deactivating quickcheck narrowing examples to find out if this causes the system error on the current isatest
bulwahn
parents: 48267
diff changeset
    15
*)