src/ZF/UNITY/ROOT.ML
author aspinall
Fri, 30 Sep 2005 18:18:34 +0200
changeset 17740 fc385ce6187d
parent 14095 a1ba833d6b61
child 23912 039ae566a4a2
permissions -rw-r--r--
Add icon for interface.

(*  Title:      ZF/UNITY/ROOT
    ID:         $Id$
    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";