src/HOL/HOL.ML
2006-11-15 haftmann 2006-11-15 removed HOL_css
2006-11-03 haftmann 2006-11-03 dropped prop_cs
2006-10-13 haftmann 2006-10-13 lifted claset setup from ML to Isar level
2006-10-11 haftmann 2006-10-11 cleaned up HOL bootstrap
2006-10-10 haftmann 2006-10-10 cleanup basic HOL bootstrap
2006-02-03 haftmann 2006-02-03 no toplevel 'thy' anymore
2005-09-06 wenzelm 2005-09-06 axclass: name space prefix is now "c_class" instead of just "c";
2005-02-10 nipkow 2005-02-10 Moved oderings from HOL into the new Orderings.thy
2003-10-09 skalberg 2003-10-09 Added support for making constants final, that is, ensuring that no definition can be given later (useful for constants whose behaviour is fixed axiomatically rather than definitionally).
2002-10-10 berghofe 2002-10-10 Added choice_eq.
2002-03-01 wenzelm 2002-03-01 tuned;
2001-10-28 wenzelm 2001-10-28 tuned declaration of rules;
2001-10-14 wenzelm 2001-10-14 added ML bindings from former theory Ord;
2001-09-27 wenzelm 2001-09-27 AddXEs [disjI1, disjI2];
2001-07-25 paulson 2001-07-25 partial restructuring to reduce dependence on Axiom of Choice
2000-11-10 wenzelm 2000-11-10 axclass power moved to Nat.thy;
2000-10-19 wenzelm 2000-10-19 declare sym [elim?] in HOL.ML instead of Calculation.thy;
2000-10-10 wenzelm 2000-10-10 AddXEs [someI_ex];
2000-09-22 wenzelm 2000-09-22 AddXIs [equal_intr_rule];
2000-09-17 wenzelm 2000-09-17 AddXIs [ext];
2000-09-15 paulson 2000-09-15 the final renaming: selectI -> someI
2000-07-21 nipkow 2000-07-21 *** empty log message ***
1999-09-09 wenzelm 1999-09-09 AddXIs [disjI1, disjI2];
1999-08-25 wenzelm 1999-08-25 proper bootstrap of HOL theory and packages;
1999-07-19 paulson 1999-07-19 getting rid of qed_goal
1999-07-10 wenzelm 1999-07-10 handle THM/TERM exn;
1999-04-27 wenzelm 1999-04-27 hol_setup;
1999-04-15 nipkow 1999-04-15 Added new thms.
1999-02-03 wenzelm 1999-02-03 ThmDatabase.ml_store_thm;
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1998-11-16 wenzelm 1998-11-16 attrib_setup: rulify;
1998-11-09 paulson 1998-11-09 removed obsolete comment and "open" declaration
1998-10-23 berghofe 1998-10-23 Added theorems True_not_False and False_not_True (for rep_datatype).
1998-09-09 nipkow 1998-09-09 Proved and added rewrite rule (@x. x=y) = y to simpset. Strange that only the symetric version was present!
1998-08-20 paulson 1998-08-20 Now qed_spec_mp respects locales, by calling ml_store_thm instead of bind_thm
1998-08-13 paulson 1998-08-13 stac now handles definitions as well as equalities
1998-08-12 oheimb 1998-08-12 added Eps_eq
1998-07-31 wenzelm 1998-07-31 isatool expandshort;
1998-07-24 berghofe 1998-07-24 Added theorem ex1_implies_ex.
1998-07-17 paulson 1998-07-17 tidying
1998-07-14 paulson 1998-07-14 stac now uses CHANGED_GOAL and correctly fails when it has no useful effect, even for conditional rewrites
1998-01-08 oheimb 1998-01-08 removed Eps_eq, ex1_Eps_eq, and some unnecessary parentheses
1997-12-23 paulson 1997-12-23 New rules rev_iffD{1,2}
1997-11-26 paulson 1997-11-26 Added rule impCE'
1997-11-04 oheimb 1997-11-04 added theorems for Eps
1997-11-03 wenzelm 1997-11-03 use "hologic.ML"; use "cladata.ML"; use "simpdata.ML"; moved to ROOT.ML;
1997-10-28 wenzelm 1997-10-28 fixed qed;
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-08-10 nipkow 1997-08-10 Added select1_equality
1997-08-06 wenzelm 1997-08-06 tuned comments;
1997-08-06 berghofe 1997-08-06 Moved some functions which used to be part of thy_data.ML
1997-06-13 nipkow 1997-06-13 Tuned wf_iff_no_infinite_down_chain proof, based on Konrads ideas. Added selectI2EX.
1997-04-21 paulson 1997-04-21 New introduction rule for "unique existence"
1997-01-29 paulson 1997-01-29 Moved qed_spec_mp, etc., from HOL.ML to thy_data.ML so that they work properly in children databases
1996-12-18 oheimb 1996-12-18 added qed_goal_spec_mp and qed_goalw_spec_mp
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-09-12 paulson 1996-09-12 Split off classical reasoning code to cladata.ML
1996-08-19 paulson 1996-08-19 Improved comment
1996-06-28 paulson 1996-06-28 Added rev_notE by analogy with rev_mp
1996-05-07 berghofe 1996-05-07 Added function for storing default claset in theory.