adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
use_thys [
"Find_Unused_Assms_Examples",
"Quickcheck_Examples",
"Quickcheck_Lattice_Examples",
"Completeness",
"Quickcheck_Interfaces",
"Hotel_Example",
"Needham_Schroeder_No_Attacker_Example"
];
if getenv "ISABELLE_GHC" = "" then ()
else use_thy "Quickcheck_Narrowing_Examples";