Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/UNITY/ROOT.ML
author wenzelm
Mon, 06 Feb 2006 20:59:10 +0100
changeset 18943 947d3a694654
parent 14095 a1ba833d6b61
child 23912 039ae566a4a2
permissions -rw-r--r--
moved no_vars to sign.ML; removed dest_def (cf. Sign.cert_def);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset 
     1
 
(*  Title:      ZF/UNITY/ROOT
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset 
     2
 
    ID:         $Id$
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset 
     3
 
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset 
     4
 
    Copyright   1998  University of Cambridge
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset 
     5
 












697dcaaf478f
new ZF/UNITY theory



paulson


parents: 

diff
changeset




     6


Root file for ZF/UNITY proofs.













697dcaaf478f
new ZF/UNITY theory



paulson


parents: 

diff
changeset




     7


*)













697dcaaf478f
new ZF/UNITY theory



paulson


parents: 

diff
changeset




     8









14046






6616e6c53d48
updating ZF-UNITY with Sidi's new material



paulson


parents: 
12198

diff
changeset




     9


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













6616e6c53d48
updating ZF-UNITY with Sidi's new material



paulson


parents: 
12198

diff
changeset




    10









14052






e9c9f69e4f63
some new ZF/UNITY material from Sidi Ehmety



paulson


parents: 
14046

diff
changeset




    11


(*Simple examples: no composition*)













e9c9f69e4f63
some new ZF/UNITY material from Sidi Ehmety



paulson


parents: 
14046

diff
changeset




    12


time_use_thy"Mutex";













e9c9f69e4f63
some new ZF/UNITY material from Sidi Ehmety



paulson


parents: 
14046

diff
changeset




    13









11479






697dcaaf478f
new ZF/UNITY theory



paulson


parents: 

diff
changeset




    14


(*Basic meta-theory*)













697dcaaf478f
new ZF/UNITY theory



paulson


parents: 

diff
changeset




    15


time_use_thy "Guar";













697dcaaf478f
new ZF/UNITY theory



paulson


parents: 

diff
changeset




    16









14095






a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new



paulson


parents: 
14060

diff
changeset




    17


(* Prefix relation; the Allocator example *)








14052






e9c9f69e4f63
some new ZF/UNITY material from Sidi Ehmety



paulson


parents: 
14046

diff
changeset




    18


time_use_thy "Distributor";








14053






4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl



paulson


parents: 
14052

diff
changeset




    19


time_use_thy "Merge";













4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl



paulson


parents: 
14052

diff
changeset




    20


time_use_thy "ClientImpl";








14060






c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas



paulson


parents: 
14053

diff
changeset




    21


time_use_thy "AllocImpl";















isabelle