doc-src/HOL/HOL.tex
2011-06-08 wenzelm 2011-06-08 merged
2011-05-30 paulson 2011-05-30 Workaround for bug involving makeindex, hyperref and the | symbol
2011-06-03 wenzelm 2011-06-03 removed some old stuff;
2011-05-26 wenzelm 2011-05-26 moved/updated basic HOL overview;
2011-05-26 wenzelm 2011-05-26 updated and re-unified (co)inductive definitions in HOL; modernized examples;
2011-05-26 wenzelm 2011-05-26 clarified current 'primrec' vs. old 'recdef'; updated examples from src/HOL/Induct;
2011-05-26 wenzelm 2011-05-26 updated and simplified HOL datatype examples (NB: special treatment of distinctness has been discontinued in the vicinity of 542b34b178ec);
2011-05-26 wenzelm 2011-05-26 updated and re-unified HOL rep_datatype;
2011-05-25 wenzelm 2011-05-25 updated and re-unified HOL typedef, with some live examples;
2011-05-03 wenzelm 2011-05-03 removed odd historical material;
2011-05-02 wenzelm 2011-05-02 eliminated old CVS Ids;
2011-05-02 wenzelm 2011-05-02 removed obsolete rail diagrams (which were about old-style theory syntax);
2011-05-02 wenzelm 2011-05-02 moved material about old codegen to isar-ref manual; eliminated old rail diagram;
2009-05-11 haftmann 2009-05-11 qualified names for Lin_Arith tactics and simprocs
2009-03-23 haftmann 2009-03-23 moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
2008-07-03 haftmann 2008-07-03 adjusted rep_datatype
2007-05-10 haftmann 2007-05-10 consts in consts_code Isar commands are now referred to by usual term syntax
2005-09-27 berghofe 2005-09-27 Tuned.
2005-09-26 berghofe 2005-09-26 Updated description of code generator.
2005-01-24 paulson 2005-01-24 updated description of arith_tac
2003-05-13 kleing 2003-05-13 HOL-Real -> HOL-Complex
2003-05-12 kleing 2003-05-12 moved % comments out of ttboxes
2002-03-06 wenzelm 2002-03-06 tuned;
2002-03-04 wenzelm 2002-03-04 hide SVC stuff (outdated); moved records to isar-ref;
2002-03-04 berghofe 2002-03-04 Added some examples to section on executable specifications.
2001-12-31 berghofe 2001-12-31 Added section on code generator.
2001-11-14 wenzelm 2001-11-14 inductive: removed con_defs;
2001-04-09 paulson 2001-04-09 lexicographic product of two relations: updated HOL.tex Also automatic updates by xemacs
2000-09-28 wenzelm 2000-09-28 record proof tools: t.equality; inductibe: split_asm, splits, cases; tuned;
2000-09-21 wenzelm 2000-09-21 renamed HOL/ex/Points to HOL/ex/Records;
2000-09-15 paulson 2000-09-15 renamed (most of...) the select rules
2000-08-28 wenzelm 2000-08-28 proper setup of iman.sty/extra.sty/ttbox.sty;
2000-07-06 paulson 2000-07-06 fixed typos reported by Jeremy Dawson
2000-06-30 paulson 2000-06-30 overloading, axclasses, numerals and general tidying
2000-03-31 nipkow 2000-03-31 updated recdef
2000-03-29 nipkow 2000-03-29 *** empty log message ***
2000-03-13 wenzelm 2000-03-13 renamed cases_tac to case_tac;
2000-03-13 nipkow 2000-03-13 exhaust -> cases
1999-10-13 berghofe 1999-10-13 Eliminated mutual_induct_tac.
1999-10-11 berghofe 1999-10-11 - Documented monotonicity theorems. - Tuned accessible part example.
1999-09-06 oheimb 1999-09-06 added smp_tac
1999-08-23 wenzelm 1999-08-23 record_simproc;
1999-08-23 berghofe 1999-08-23 Some changes in sections about Sum and Nat.
1999-08-19 paulson 1999-08-19 documented svc_tac
1999-08-17 wenzelm 1999-08-17 eliminated HOL_quantifiers (replaced by "HOL" print mode);
1999-07-19 berghofe 1999-07-19 Documented usage of function types in datatype specifications.
1999-05-10 wenzelm 1999-05-10 tuned;
1999-05-10 wenzelm 1999-05-10 pdf setup;
1999-05-05 paulson 1999-05-05 Now uses manual.bib; some references updated
1999-05-05 nipkow 1999-05-05 Bibtex stuff.
1999-05-04 wenzelm 1999-05-04 used to be part of 'logics' manual;