doc-src/HOL/HOL.tex
2001-11-14 ago inductive: removed con_defs;
2001-04-09 ago lexicographic product of two relations: updated HOL.tex
2000-09-28 ago record proof tools: t.equality;
2000-09-21 ago renamed HOL/ex/Points to HOL/ex/Records;
2000-09-15 ago renamed (most of...) the select rules
2000-08-28 ago proper setup of iman.sty/extra.sty/ttbox.sty;
2000-07-06 ago fixed typos reported by Jeremy Dawson
2000-06-30 ago overloading, axclasses, numerals and general tidying
2000-03-31 ago updated recdef
2000-03-29 ago *** empty log message ***
2000-03-13 ago renamed cases_tac to case_tac;
2000-03-13 ago exhaust -> cases
1999-10-13 ago Eliminated mutual_induct_tac.
1999-10-11 ago - Documented monotonicity theorems.
1999-09-06 ago added smp_tac
1999-08-23 ago record_simproc;
1999-08-23 ago Some changes in sections about Sum and Nat.
1999-08-19 ago documented svc_tac
1999-08-17 ago eliminated HOL_quantifiers (replaced by "HOL" print mode);
1999-07-19 ago Documented usage of function types in datatype specifications.
1999-05-10 ago tuned;
1999-05-10 ago pdf setup;
1999-05-05 ago Now uses manual.bib; some references updated
1999-05-05 ago Bibtex stuff.
1999-05-04 ago used to be part of 'logics' manual;