(*  Title:      HOL/UNITY/ROOT
    ID:         $Id: ROOT.ML,v 1.33 2003/09/23 13:49:17 paulson Exp $
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

Root file for UNITY proofs.
*)

(*Basic meta-theory*)
time_use_thy "UNITY_Main";

(*Simple examples: no composition*)
time_use_thy "Simple/Deadlock";
time_use_thy "Simple/Common";
time_use_thy "Simple/Network";
time_use_thy "Simple/Token";
time_use_thy "Simple/Channel";
time_use_thy "Simple/Lift";
time_use_thy "Simple/Mutex";
time_use_thy "Simple/Reach";
time_use_thy "Simple/Reachability";

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

(*Example of composition*)
time_use_thy "Comp/Handshake";

(*Universal properties examples*)
time_use_thy "Comp/Counter";
time_use_thy "Comp/Counterc";
time_use_thy "Comp/Priority";

time_use_thy "Comp/TimerArray";

(*Allocator example*)
time_use_thy "Comp/Alloc";
time_use_thy "Comp/AllocImpl";
time_use_thy "Comp/Client";

time_use_thy "ELT";  (*obsolete*)
