src/HOL/hologic.ML
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;
2000-02-22 wenzelm 2000-02-22 added boolN;
2000-01-05 wenzelm 2000-01-05 replaced HOLogic.termTVar by HOLogic.termT;
1999-10-04 wenzelm 1999-10-04 added mk_conj, mk_disj, mk_imp;
1999-09-21 nipkow 1999-09-21 ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
1999-08-03 paulson 1999-08-03 added realT
1999-07-23 paulson 1999-07-23 added boolean and binary constants
1999-03-17 wenzelm 1999-03-17 added dest_mem;
1998-12-18 paulson 1998-12-18 new function dest_eq
1998-07-28 wenzelm 1998-07-28 tuned;
1998-06-30 berghofe 1998-06-30 Moved most of the Prod_Syntax - stuff to HOLogic.
1998-01-14 wenzelm 1998-01-14 added unit and prod stuff;
1997-12-23 paulson 1997-12-23 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
1997-11-26 wenzelm 1997-11-26 added dest_nat;
1997-10-06 wenzelm 1997-10-06 eliminated raise_term, raise_typ;
1997-01-16 wenzelm 1997-01-16 binary oprations and relations; nat;
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application