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
lcp [Thu, 18 Aug 1994 12:07:51 +0200] rev 109
HOL/Nat: rotated arguments of nat_case; added translation for case macro
HOL/Nat/nat_ss0: new, for first definition of nat_ss
lcp [Thu, 18 Aug 1994 11:54:20 +0200] rev 108
HOL/Trancl: comp_cs is based upon prod_cs; tidied proofs
lcp [Thu, 18 Aug 1994 11:43:40 +0200] rev 107
HOL/Sum: rotated arguments of sum_case; added translation for case macro
HOL/Sum: now has Part primitives, moved from ex/Simult, with extra
laws from ZF/Sum
lcp [Thu, 18 Aug 1994 11:40:54 +0200] rev 106
HOL/Subst/AList: swapped args of split and simplified
lcp [Thu, 18 Aug 1994 11:30:27 +0200] rev 105
HOL/LList: swapped args of split and simplified
HOL/List: rotated arguments of List_case, list_case
HOL/LList: rotated arguments of llist_case (shares List_case) and tidied
many proofs
nipkow [Tue, 16 Aug 1994 09:57:51 +0200] rev 104
allow long_id for reference to type in primrec.
Doesn't work yet, though, because of problems with the autoloader.