src/HOL/Hilbert_Choice.thy
Wed, 28 Jan 2009 11:03:42 +0100 haftmann Plain, Main form meeting points in import hierarchy
Wed, 06 Aug 2008 13:57:25 +0200 nipkow added lemma
Fri, 25 Apr 2008 15:30:33 +0200 krauss Merged theories about wellfoundedness into one: Wellfounded.thy
Mon, 07 Apr 2008 15:37:27 +0200 paulson * Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
Thu, 20 Mar 2008 12:01:09 +0100 haftmann tuned proofs
Thu, 21 Feb 2008 17:33:58 +0100 nipkow moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
Fri, 15 Feb 2008 16:09:12 +0100 haftmann <= and < on nat no longer depend on wellfounded relations
Wed, 20 Jun 2007 14:38:24 +0200 nipkow added lemmas
Sun, 15 Apr 2007 14:31:44 +0200 wenzelm replaced axioms/finalconsts by proper axiomatization;
Thu, 04 Jan 2007 17:55:12 +0100 paulson improvements to proof reconstruction. Some files loaded in a different order
Wed, 08 Nov 2006 13:48:29 +0100 wenzelm removed theory NatArith (now part of Nat);
Fri, 13 Oct 2006 18:15:18 +0200 berghofe Adapted to changes in FixedPoint theory.
Tue, 13 Dec 2005 15:27:43 +0100 paulson removal of functional reflexivity axioms
Tue, 18 Oct 2005 17:59:26 +0200 wenzelm added lemma exE_some (from specification_package.ML);
Thu, 29 Sep 2005 00:58:55 +0200 wenzelm more finalconsts;
Thu, 15 Sep 2005 17:44:53 +0200 paulson comment
Wed, 13 Jul 2005 15:06:20 +0200 paulson generlization of some "nat" theorems
Fri, 24 Jun 2005 17:25:10 +0200 paulson meson method taking an argument list
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Tue, 19 Oct 2004 18:18:45 +0200 paulson converted some induct_tac to induct
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax.
Sat, 05 Jun 2004 13:07:04 +0200 wenzelm improved symbolic syntax of Eps: \<some> for mode "epsilon";
Wed, 19 May 2004 11:29:47 +0200 paulson conversion of Hilbert_Choice to Isar script
Thu, 19 Feb 2004 16:44:21 +0100 ballarin New lemmas about inversion of restricted functions.
Fri, 26 Sep 2003 10:34:57 +0200 paulson misc tidying
Thu, 17 Jul 2003 15:23:20 +0200 skalberg Added package for definition by specification.
Sun, 22 Dec 2002 15:02:40 +0100 nipkow removed some problems with print translations
Sun, 22 Dec 2002 10:43:43 +0100 nipkow added print translations tha avoid eta contraction for important binders.
Thu, 26 Sep 2002 10:51:29 +0200 paulson Converted Fun to Isar style.
Wed, 05 Dec 2001 03:07:44 +0100 wenzelm tuned declarations;
Mon, 26 Nov 2001 18:33:57 +0100 wenzelm tuned;
Sat, 03 Nov 2001 01:33:54 +0100 wenzelm tuned;
Wed, 29 Aug 2001 21:17:24 +0200 wenzelm avoid ML bindings;
Wed, 25 Jul 2001 17:58:26 +0200 paulson Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
Wed, 25 Jul 2001 13:13:01 +0200 paulson partial restructuring to reduce dependence on Axiom of Choice
less more (0) tip