src/HOL/HOL.ML
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.
1996-04-23 oheimb 1996-04-23 repaired critical proofs depending on the order inside non-confluent SimpSets, (temporarily) removed problematic rule less_Suc_eq form simpset_of "Nat"
1996-04-19 clasohm 1996-04-19 added Konrad's code for the datatype package
1996-04-17 oheimb 1996-04-17 *** empty log message ***
1996-04-12 clasohm 1996-04-12 changed first parameter of add_thydata and get_thydata
1996-02-19 nipkow 1996-02-19 Introduced normalize_thm into HOL.ML Corrected some dependencies among Sum, Prod and mono. Extended RelPow
1996-02-09 nipkow 1996-02-09 Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
1996-01-30 clasohm 1996-01-30 expanded tabs
1996-01-29 clasohm 1996-01-29 changed the way simpsets and information about datatypes are stored
1995-11-17 clasohm 1995-11-17 changed simpset of "HOL"
1995-11-16 nipkow 1995-11-16 added rev_contrapos
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application