Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
 
*)
isabelle