| Tue, 27 May 2003 17:39:17 +0200 | berghofe | Added pair_const. | file | diff | annotate |
| Mon, 16 Dec 2002 13:43:11 +0100 | berghofe | Added mk_int and mk_list. | file | diff | annotate |
| Mon, 09 Dec 2002 10:38:56 +0100 | ballarin | Fixed bug in simpdata.ML that prevented the use of congruence rules from a | file | diff | annotate |
| Thu, 10 Oct 2002 14:23:47 +0200 | berghofe | Added list_all. | file | diff | annotate |
| Sat, 01 Dec 2001 18:52:32 +0100 | wenzelm | renamed class "term" to "type" (actually "HOL.type"); | file | diff | annotate |
| Wed, 17 Oct 2001 18:51:03 +0200 | wenzelm | added mk_UNIV; | file | diff | annotate |
| Thu, 04 Oct 2001 15:40:05 +0200 | wenzelm | added dest_concls; | file | diff | annotate |
| Thu, 27 Sep 2001 22:23:40 +0200 | wenzelm | made unit type local; | file | diff | annotate |
| Mon, 18 Dec 2000 14:59:05 +0100 | nipkow | moved mk_bin from Numerals to HOLogic | file | diff | annotate |
| Fri, 03 Nov 2000 21:31:53 +0100 | wenzelm | removed atomic_Trueprop (now in Pure/Isar/auto_bind.ML); | file | diff | annotate |
| Tue, 05 Sep 2000 18:48:22 +0200 | wenzelm | added not_const; | file | diff | annotate |
| Sun, 30 Jul 2000 13:02:14 +0200 | wenzelm | added atomic_Trueprop; | file | diff | annotate |
| Sun, 16 Jul 2000 20:54:24 +0200 | wenzelm | added is_unitT; | file | diff | annotate |
| Sun, 23 Apr 2000 11:39:56 +0200 | paulson | number_of now takes a type arg | file | diff | annotate |
| Tue, 18 Apr 2000 15:54:56 +0200 | paulson | added number_of_const: term | file | diff | annotate |
| Mon, 13 Mar 2000 13:17:52 +0100 | wenzelm | added Not; | file | diff | annotate |
| Sun, 27 Feb 2000 15:22:14 +0100 | wenzelm | added dest_conj; | file | diff | annotate |
| Tue, 22 Feb 2000 21:39:01 +0100 | wenzelm | added boolN; | file | diff | annotate |
| Wed, 05 Jan 2000 11:56:04 +0100 | wenzelm | replaced HOLogic.termTVar by HOLogic.termT; | file | diff | annotate |
| Mon, 04 Oct 1999 14:45:35 +0200 | wenzelm | added mk_conj, mk_disj, mk_imp; | file | diff | annotate |
| Tue, 21 Sep 1999 14:13:45 +0200 | nipkow | ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML | file | diff | annotate |
| Tue, 03 Aug 1999 13:15:20 +0200 | paulson | added realT | file | diff | annotate |
| Fri, 23 Jul 1999 17:25:27 +0200 | paulson | added boolean and binary constants | file | diff | annotate |
| Wed, 17 Mar 1999 13:46:23 +0100 | wenzelm | added dest_mem; | file | diff | annotate |
| Fri, 18 Dec 1998 11:00:15 +0100 | paulson | new function dest_eq | file | diff | annotate |
| Tue, 28 Jul 1998 16:59:15 +0200 | wenzelm | tuned; | file | diff | annotate |
| Tue, 30 Jun 1998 20:41:41 +0200 | berghofe | Moved most of the Prod_Syntax - stuff to HOLogic. | file | diff | annotate |
| Wed, 14 Jan 1998 10:30:44 +0100 | wenzelm | added unit and prod stuff; | file | diff | annotate |
| Tue, 23 Dec 1997 11:39:03 +0100 | paulson | Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac | file | diff | annotate |
| Wed, 26 Nov 1997 16:43:42 +0100 | wenzelm | added dest_nat; | file | diff | annotate |
| Mon, 06 Oct 1997 19:15:02 +0200 | wenzelm | eliminated raise_term, raise_typ; | file | diff | annotate |
| Thu, 16 Jan 1997 16:53:15 +0100 | wenzelm | binary oprations and relations; | file | diff | annotate |
| Fri, 03 Mar 1995 12:02:25 +0100 | clasohm | new version of HOL with curried function application | file | diff | annotate |