doc-src/ind-defs.tex
1996-11-22 paulson 1996-11-22 Minor textual improvements; updating of a reference
1996-10-30 paulson 1996-10-30 Minor updates
1996-07-17 paulson 1996-07-17 Edited in response to referees comments; new references
1996-05-09 paulson 1996-05-09 Updated for new form of induction rules
1996-03-04 paulson 1996-03-04 Revised for publication. Removed LNCS style. Discussion of recent work.
1995-12-22 paulson 1995-12-22 Note that unfold is not exported, that mutual_induct can be omitted (as the trivial theorem True), and comments on storage Also uses Datatype instead of Univ/Quniv as parent theory for lists, and omits quotes around types in theory files.
1995-07-26 lcp 1995-07-26 trivial updates to header and bibliography
1994-09-09 lcp 1994-09-09 Updated for existence of HOL version and infinitely branching datatypes
1994-09-06 lcp 1994-09-06 documentation of theory sections (co)inductive and (co)datatype
1994-07-29 lcp 1994-07-29 revised for new theory system: removal of ext, addition of thy_name
1994-07-11 lcp 1994-07-11 misc updates
1994-05-03 lcp 1994-05-03 post-CRC corrections
1993-12-02 lcp 1993-12-02 removal of amssymbols.sty and lcp.sty; addition of iman.sty
1993-12-01 lcp 1993-12-01 minor corrections
1993-11-19 lcp 1993-11-19 Many edits suggested by Grundy & Thompson
1993-11-09 lcp 1993-11-09 Initial revision