author wenzelm
Wed, 08 Oct 2008 19:20:29 +0200
changeset 28529 7ff939586e83
parent 24147 edc90be09ac1
child 28866 30cd9d89a0fb
permissions -rw-r--r--
setmp_noncritical makes it work with future scheduler;

(*  Title:      HOL/UNITY/ROOT
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

Root file for UNITY proofs.

(*Verifying security protocols using UNITY*)
no_document use_thy "../Auth/Public";

use_thys [
  (*Basic meta-theory*)

  (*Simple examples: no composition*)

  (*Verifying security protocols using UNITY*)

  (*Example of composition*)

  (*Universal properties examples*)



(*Allocator example*)
(* FIXME some parts no longer work -- had been commented out for a long time *)
setmp_noncritical quick_and_dirty true
  use_thy "Comp/Alloc";

use_thys ["Comp/AllocImpl", "Comp/Client"];