author | paulson |
Fri, 20 Jun 2003 12:10:45 +0200 | |
changeset 14060 | c0c4af41fa3b |
parent 14053 | 4daa384f4fd7 |
child 14095 | a1ba833d6b61 |
permissions | -rw-r--r-- |
(* 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; part of the Allocator example *) time_use_thy "GenPrefix"; time_use_thy "Distributor"; time_use_thy "Merge"; time_use_thy "ClientImpl"; time_use_thy "AllocImpl";