src/ZF/UNITY/ROOT.ML
author paulson
Tue, 21 May 2002 13:06:36 +0200
changeset 13168 afcbca3498b0
parent 12198 113c1cd7a164
child 14046 6616e6c53d48
permissions -rw-r--r--
converted domrange to Isar and merged with equalities

(*  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.
*)

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

(* Prefix relation; part of the Allocator example *)
time_use_thy "GenPrefix";

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