src/HOL/hologic.ML
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