src/ZF/UNITY/ROOT.ML

HOL-Real -> HOL-Complex

(*  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";