lcp [Fri, 19 Aug 1994 11:25:16 +0200] rev 119
HOL/Makefile, ROOT: updated for new .thy files
lcp [Fri, 19 Aug 1994 11:19:14 +0200] rev 118
HOL/Ord.thy,.ML: files now have header comments
lcp [Fri, 19 Aug 1994 11:15:01 +0200] rev 117
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
overloaded with an incompatible type
lcp [Fri, 19 Aug 1994 11:10:56 +0200] rev 116
HOL/subset.thy, equalities.thy, mono.thy: new
HOL/Lfp.thy: now depends upon mono
HOL/Gfp.thy: depends upon Lfp, not just mono
lcp [Fri, 19 Aug 1994 11:02:45 +0200] rev 115
HOL/fun.ML: renamed Fun.ML to avoid problems with MLs "fun" keyword
lcp [Thu, 18 Aug 1994 12:48:03 +0200] rev 114
HOL/ex/Term, Simult: updated for new Split
lcp [Thu, 18 Aug 1994 12:42:19 +0200] rev 113
HOL/List: rotated arguments of List_case, list_case
lcp [Thu, 18 Aug 1994 12:38:12 +0200] rev 112
HOL/Prod: swapped args of split and simplified
HOL/Prod/mem_splitI, mem_splitE, prod_cs: new
lcp [Thu, 18 Aug 1994 12:23:52 +0200] rev 111
HOL/Univ: swapped args of split and simplified
HOL/Univ: simplified many proofs involving dprod, dsum.
HOL/Univ: updated to new nat_case
HOL/Univ/univ_cs: added to it and used it more
lcp [Thu, 18 Aug 1994 12:13:26 +0200] rev 110
HOL/Sexp: rotated arguments of Sexp_case