doc-src/Logics/Old_HOL.tex
2000-08-28 wenzelm 2000-08-28 proper setup of iman.sty/extra.sty/ttbox.sty;
1997-04-17 paulson 1997-04-17 Corrected the informal description of coinductive definition
1995-05-03 lcp 1995-05-03 trivial change
1995-01-13 lcp 1995-01-13 Corrected indexing of *datatype
1995-01-02 wenzelm 1995-01-02 fixed minor typos;
1994-11-11 lcp 1994-11-11 removal of HOL_dup_cs rotation of arguments in split, nat_case, sum_case, list_case
1994-10-12 lcp 1994-10-12 Moving theory LList to ex directory
1994-09-11 nipkow 1994-09-11 Added primrec section.
1994-09-09 lcp 1994-09-09 Logics/HOL: Section 3, added Pow and its rule. New sections 6 on the datatype declaration and 7 on (co)inductive definitions. Added mention of directory IMP.
1994-08-31 nipkow 1994-08-31 Updated datatype documentation with a few hints
1994-07-13 lcp 1994-07-13 indentation and renaming of rules
1994-07-12 nipkow 1994-07-12 Corrected HOL.tex
1994-07-12 nipkow 1994-07-12 added datatype section
1994-07-07 nipkow 1994-07-07 added () around some of the ::
1994-05-03 lcp 1994-05-03 post-CRC corrections
1994-04-25 lcp 1994-04-25 final Springer copy
1994-04-15 lcp 1994-04-15 penultimate Springer draft
1994-03-30 nipkow 1994-03-30 changed lists and added "let" and "case"
1994-03-21 lcp 1994-03-21 first draft of Springer book
1993-11-25 wenzelm 1993-11-25 corrected obvious errors;
1993-11-12 lcp 1993-11-12 Misc updates
1993-11-11 lcp 1993-11-11 Various updates for Isabelle-93
1993-11-10 lcp 1993-11-10 Initial revision