(*  Title:      ZF/UNITY/ROOT
    ID:         $Id: ROOT.ML,v 1.7 2003/07/10 15:14:42 paulson Exp $
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

Root file for ZF/UNITY proofs.
*)

add_path "../Induct";  (*for Multisets*)

(*Simple examples: no composition*)
time_use_thy"Mutex";

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

(* Prefix relation; the Allocator example *)
time_use_thy "Distributor";
time_use_thy "Merge";
time_use_thy "ClientImpl";
time_use_thy "AllocImpl";