src/HOL/hologic.ML
2007-09-18 wenzelm 2007-09-18 simplified type int (eliminated IntInf.int, integer);
2007-07-11 berghofe 2007-07-11 New operations on tuples with specific arities.
2007-07-05 wenzelm 2007-07-05 removed dest_cTrueprop (cf. ObjectLogic.dest_judgment);
2007-07-04 wenzelm 2007-07-04 replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
2007-07-03 wenzelm 2007-07-03 assume basic HOL context for compilation (antiquotations); added dest_cTrueprop; tuned Trueprop_conv; added low-level conj_intr/elim/elis (dire need for @{rule} antiquotation!);
2007-06-09 wenzelm 2007-06-09 simplified type integer;
2007-06-05 wenzelm 2007-06-05 simplified/renamed add_numerals;
2007-06-05 haftmann 2007-06-05 merged Code_Generator.thy into HOL.thy
2007-05-17 haftmann 2007-05-17 abstract size function in hologic.ML
2007-03-02 haftmann 2007-03-02 added add_numerals_of
2006-12-13 wenzelm 2006-12-13 simplified mk/dest_numeral (cf. mk/dest_binum of 1.65); put signature into canonical order;
2006-12-13 haftmann 2006-12-13 introduced mk/dest_numeral/number for mk/dest_binum etc.
2006-12-12 wenzelm 2006-12-12 made SML/NJ happy;
2006-12-12 wenzelm 2006-12-12 binary numerals: restricted to actual abstract syntax; tuned;
2006-12-10 wenzelm 2006-12-10 misc cleanup -- removed non-HOL operations; nibble/char/list/string: observe conventions for abstract syntax operations;
2006-12-01 haftmann 2006-12-01 slight cleanup in hologic.ML
2006-11-27 haftmann 2006-11-27 added Trueprop_conv
2006-11-23 wenzelm 2006-11-23 removed dead code;
2006-11-22 haftmann 2006-11-22 incorporated structure HOList into HOLogic
2006-11-07 wenzelm 2006-11-07 removed obsolete dest_eq_typ;
2006-11-04 wenzelm 2006-11-04 removed is_Trueprop (use can dest_Trueprop'' instead); tuned list_all;
2006-10-20 haftmann 2006-10-20 slight cleanup
2006-10-16 haftmann 2006-10-16 slight cleanup
2006-10-11 haftmann 2006-10-11 cleaned up HOL bootstrap
2006-10-02 paulson 2006-10-02 added is_Trueprop
2006-09-26 haftmann 2006-09-26 renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
2006-09-06 haftmann 2006-09-06 got rid of Numeral.bin type
2006-04-27 paulson 2006-04-27 renamed HOLogic.mk_bin to mk_binum for consistency with dest_binum
2005-11-29 wenzelm 2005-11-29 added mk_split;
2005-08-16 nipkow 2005-08-16 added listT
2005-08-01 wenzelm 2005-08-01 removed read_cterm; tuned;
2005-07-14 wenzelm 2005-07-14 removed not_const -- use Not instead; add mk_not;
2005-05-16 paulson 2005-05-16 Use of IntInf.int instead of int in most numeric simprocs; avoids integer overflow in SML/NJ
2005-05-09 paulson 2005-05-09 choice_const moved to hologic.ML
2005-03-23 paulson 2005-03-23 replaced bool by a new datatype "bit" for binary numerals
2005-03-08 obua 2005-03-08 fix integer overflow in numeral syntax for SML NJ.
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2004-08-20 paulson 2004-08-20 proof reconstruction for external ATPs
2004-07-19 berghofe 2004-07-19 Added function dest_list.
2004-07-01 paulson 2004-07-01 new treatment of binary numerals
2004-02-15 paulson 2004-02-15 Polymorphic treatment of binary arithmetic using axclasses
2003-07-11 berghofe 2003-07-11 mk_int now produces specific constants for 0 and 1.
2003-05-27 berghofe 2003-05-27 Added pair_const.
2002-12-16 berghofe 2002-12-16 Added mk_int and mk_list.
2002-12-09 ballarin 2002-12-09 Fixed bug in simpdata.ML that prevented the use of congruence rules from a locale. (mk_meta_cong did wrongly convert metahyps to hyps)
2002-10-10 berghofe 2002-10-10 Added list_all.
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-10-17 wenzelm 2001-10-17 added mk_UNIV;
2001-10-04 wenzelm 2001-10-04 added dest_concls;
2001-09-27 wenzelm 2001-09-27 made unit type local;
2000-12-18 nipkow 2000-12-18 moved mk_bin from Numerals to HOLogic first steps towards rational lin arith
2000-11-03 wenzelm 2000-11-03 removed atomic_Trueprop (now in Pure/Isar/auto_bind.ML);
2000-09-05 wenzelm 2000-09-05 added not_const;
2000-07-30 wenzelm 2000-07-30 added atomic_Trueprop;
2000-07-16 wenzelm 2000-07-16 added is_unitT; added proper versions of mk_tuple(T), dest_tuple(T) -- unused;
2000-04-23 paulson 2000-04-23 number_of now takes a type arg
2000-04-18 paulson 2000-04-18 added number_of_const: term
2000-03-13 wenzelm 2000-03-13 added Not;
2000-02-27 wenzelm 2000-02-27 added dest_conj;