doc-src/TutorialI/Protocol/ROOT.ML
author bulwahn
Sun, 04 Dec 2011 20:05:08 +0100
changeset 45750 17100f4ce0b5
parent 42637 381fdcab0f36
permissions -rw-r--r--
adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e); adjusting smart quickcheck compilation to new signature of exhaustive generators (cf. 1f5fc44254d7);

(*
To update:
cp /home/lcp/isabelle/Repos/HOL/Auth/{Message.thy,Message_lemmas.ML,Event.thy,Event_lemmas.ML,Public.thy,Public_lemmas.ML,NS_Public.thy} .
*)

use_thy "NS_Public";