src/HOL/HOL.ML
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