src/HOL/HOL.ML
Thu, 09 Oct 2003 18:13:32 +0200 skalberg Added support for making constants final, that is, ensuring that no
Thu, 10 Oct 2002 14:21:49 +0200 berghofe Added choice_eq.
Fri, 01 Mar 2002 22:28:59 +0100 wenzelm tuned;
Sun, 28 Oct 2001 21:14:56 +0100 wenzelm tuned declaration of rules;
Sun, 14 Oct 2001 20:00:32 +0200 wenzelm added ML bindings from former theory Ord;
Thu, 27 Sep 2001 16:04:11 +0200 wenzelm AddXEs [disjI1, disjI2];
Wed, 25 Jul 2001 13:13:01 +0200 paulson partial restructuring to reduce dependence on Axiom of Choice
Fri, 10 Nov 2000 19:03:06 +0100 wenzelm axclass power moved to Nat.thy;
Thu, 19 Oct 2000 21:20:53 +0200 wenzelm declare sym [elim?] in HOL.ML instead of Calculation.thy;
Tue, 10 Oct 2000 23:43:23 +0200 wenzelm AddXEs [someI_ex];
Fri, 22 Sep 2000 17:24:36 +0200 wenzelm AddXIs [equal_intr_rule];
Sun, 17 Sep 2000 22:24:52 +0200 wenzelm AddXIs [ext];
Fri, 15 Sep 2000 15:30:50 +0200 paulson the final renaming: selectI -> someI
Fri, 21 Jul 2000 12:30:08 +0200 nipkow *** empty log message ***
Thu, 09 Sep 1999 12:25:30 +0200 wenzelm AddXIs [disjI1, disjI2];
Wed, 25 Aug 1999 20:49:02 +0200 wenzelm proper bootstrap of HOL theory and packages;
Mon, 19 Jul 1999 15:19:11 +0200 paulson getting rid of qed_goal
Sat, 10 Jul 1999 21:48:27 +0200 wenzelm handle THM/TERM exn;
Tue, 27 Apr 1999 10:43:52 +0200 wenzelm hol_setup;
Thu, 15 Apr 1999 18:10:37 +0200 nipkow Added new thms.
Wed, 03 Feb 1999 17:33:20 +0100 wenzelm ThmDatabase.ml_store_thm;
Tue, 12 Jan 1999 13:54:51 +0100 wenzelm eliminated tthm type and Attribute structure;
Mon, 16 Nov 1998 11:11:58 +0100 wenzelm attrib_setup: rulify;
Mon, 09 Nov 1998 10:58:49 +0100 paulson removed obsolete comment and "open" declaration
Fri, 23 Oct 1998 22:36:15 +0200 berghofe Added theorems True_not_False and False_not_True
Wed, 09 Sep 1998 17:34:58 +0200 nipkow Proved and added rewrite rule (@x. x=y) = y to simpset.
Thu, 20 Aug 1998 09:25:59 +0200 paulson Now qed_spec_mp respects locales, by calling ml_store_thm
Thu, 13 Aug 1998 17:28:52 +0200 paulson stac now handles definitions as well as equalities
Wed, 12 Aug 1998 15:40:47 +0200 oheimb added Eps_eq
Fri, 31 Jul 1998 11:03:31 +0200 wenzelm isatool expandshort;
Fri, 24 Jul 1998 13:27:23 +0200 berghofe Added theorem ex1_implies_ex.
Fri, 17 Jul 1998 10:50:01 +0200 paulson tidying
Tue, 14 Jul 1998 13:29:39 +0200 paulson stac now uses CHANGED_GOAL and correctly fails when it has no useful effect,
Thu, 08 Jan 1998 17:47:22 +0100 oheimb removed Eps_eq, ex1_Eps_eq, and some unnecessary parentheses
Tue, 23 Dec 1997 11:40:18 +0100 paulson New rules rev_iffD{1,2}
Wed, 26 Nov 1997 17:23:18 +0100 paulson Added rule impCE'
Tue, 04 Nov 1997 20:46:56 +0100 oheimb added theorems for Eps
Mon, 03 Nov 1997 12:11:34 +0100 wenzelm use "hologic.ML"; use "cladata.ML"; use "simpdata.ML"; moved to ROOT.ML;
Tue, 28 Oct 1997 17:41:40 +0100 wenzelm fixed qed;
Fri, 10 Oct 1997 19:02:28 +0200 wenzelm fixed dots;
Sun, 10 Aug 1997 12:28:34 +0200 nipkow Added select1_equality
Wed, 06 Aug 1997 11:57:20 +0200 wenzelm tuned comments;
Wed, 06 Aug 1997 01:13:46 +0200 berghofe Moved some functions which used to be part of thy_data.ML
Fri, 13 Jun 1997 10:35:13 +0200 nipkow Tuned wf_iff_no_infinite_down_chain proof, based on Konrads ideas.
Mon, 21 Apr 1997 12:16:04 +0200 paulson New introduction rule for "unique existence"
Wed, 29 Jan 1997 15:32:18 +0100 paulson Moved qed_spec_mp, etc., from HOL.ML to thy_data.ML so that they work
Wed, 18 Dec 1996 15:11:07 +0100 oheimb added qed_goal_spec_mp and qed_goalw_spec_mp
Thu, 26 Sep 1996 12:47:47 +0200 paulson Ran expandshort
Thu, 12 Sep 1996 10:34:01 +0200 paulson Split off classical reasoning code to cladata.ML
Mon, 19 Aug 1996 11:33:08 +0200 paulson Improved comment
Fri, 28 Jun 1996 15:27:53 +0200 paulson Added rev_notE by analogy with rev_mp
Tue, 07 May 1996 09:53:20 +0200 berghofe Added function for storing default claset in theory.
Tue, 23 Apr 1996 16:58:21 +0200 oheimb repaired critical proofs depending on the order inside non-confluent SimpSets,
Fri, 19 Apr 1996 11:33:24 +0200 clasohm added Konrad's code for the datatype package
Wed, 17 Apr 1996 17:59:58 +0200 oheimb *** empty log message ***
Fri, 12 Apr 1996 12:41:26 +0200 clasohm changed first parameter of add_thydata and get_thydata
Mon, 19 Feb 1996 18:04:41 +0100 nipkow Introduced normalize_thm into HOL.ML
Fri, 09 Feb 1996 13:41:18 +0100 nipkow Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
Tue, 30 Jan 1996 15:24:36 +0100 clasohm expanded tabs
Mon, 29 Jan 1996 13:48:37 +0100 clasohm changed the way simpsets and information about datatypes are stored
less more (0) -60 tip