Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/hologic.ML
Fri, 01 Dec 2006 17:22:31 +0100 haftmann slight cleanup in hologic.ML file | diff | annotate
Mon, 27 Nov 2006 13:42:46 +0100 haftmann added Trueprop_conv file | diff | annotate
Thu, 23 Nov 2006 00:51:47 +0100 wenzelm removed dead code; file | diff | annotate
Wed, 22 Nov 2006 10:20:15 +0100 haftmann incorporated structure HOList into HOLogic file | diff | annotate
Tue, 07 Nov 2006 14:29:58 +0100 wenzelm removed obsolete dest_eq_typ; file | diff | annotate
Sat, 04 Nov 2006 19:25:40 +0100 wenzelm removed is_Trueprop (use can dest_Trueprop'' instead); file | diff | annotate
Fri, 20 Oct 2006 17:07:26 +0200 haftmann slight cleanup file | diff | annotate
Mon, 16 Oct 2006 14:07:21 +0200 haftmann slight cleanup file | diff | annotate
Wed, 11 Oct 2006 14:51:24 +0200 haftmann cleaned up HOL bootstrap file | diff | annotate
Mon, 02 Oct 2006 17:33:13 +0200 paulson added is_Trueprop file | diff | annotate
Tue, 26 Sep 2006 13:34:16 +0200 haftmann renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes file | diff | annotate
Wed, 06 Sep 2006 13:48:02 +0200 haftmann got rid of Numeral.bin type file | diff | annotate
Thu, 27 Apr 2006 12:11:56 +0200 paulson renamed HOLogic.mk_bin to mk_binum for consistency with dest_binum file | diff | annotate
Tue, 29 Nov 2005 22:52:19 +0100 wenzelm added mk_split; file | diff | annotate
Tue, 16 Aug 2005 13:54:24 +0200 nipkow added listT file | diff | annotate
Mon, 01 Aug 2005 19:20:24 +0200 wenzelm removed read_cterm; file | diff | annotate
Thu, 14 Jul 2005 19:28:17 +0200 wenzelm removed not_const -- use Not instead; file | diff | annotate
Mon, 16 May 2005 10:29:15 +0200 paulson Use of IntInf.int instead of int in most numeric simprocs; avoids file | diff | annotate
Mon, 09 May 2005 16:40:11 +0200 paulson choice_const moved to hologic.ML file | diff | annotate
Wed, 23 Mar 2005 12:09:18 +0100 paulson replaced bool by a new datatype "bit" for binary numerals file | diff | annotate
Tue, 08 Mar 2005 16:02:52 +0100 obua fix integer overflow in numeral syntax for SML NJ. file | diff | annotate
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr. file | diff | annotate
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions. file | diff | annotate
Fri, 20 Aug 2004 12:21:03 +0200 paulson proof reconstruction for external ATPs file | diff | annotate
Mon, 19 Jul 2004 18:14:57 +0200 berghofe Added function dest_list. file | diff | annotate
Thu, 01 Jul 2004 12:29:53 +0200 paulson new treatment of binary numerals file | diff | annotate
Sun, 15 Feb 2004 10:46:37 +0100 paulson Polymorphic treatment of binary arithmetic using axclasses file | diff | annotate
Fri, 11 Jul 2003 14:56:30 +0200 berghofe mk_int now produces specific constants for 0 and 1. file | diff | annotate
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
less more (0) tip
isabelle