1998-11-16 paulson 1998-11-16 moved some facts about Pi from ex/PiSets to Fun.ML
1998-11-13 paulson 1998-11-13 the function space operator
1998-11-11 paulson 1998-11-11 proved surjI
1998-10-02 nipkow 1998-10-02 id <-> Id
1998-09-09 oheimb 1998-09-09 added Id_apply
1998-08-14 paulson 1998-08-14 expandshort
1998-08-13 paulson 1998-08-13 even more tidying of Goal commands
1998-08-12 oheimb 1998-08-12 added theorems Id_o, o_Id corrected name of theorem: fund_upd_other -> fun_upd_other
1998-08-12 oheimb 1998-08-12 cleanup for Fun.thy: merged Update.{thy|ML} into Fun.{thy|ML} moved o_def from HOL.thy to Fun.thy added Id_def to Fun.thy moved image_compose from Set.ML to Fun.ML moved o_apply and o_assoc from simpdata.ML to Fun.ML moved fun_upd_same and fun_upd_other (from Map.ML) to Fun.ML added fun_upd_twist to Fun.ML
1998-07-15 paulson 1998-07-15 More tidying and removal of "\!\!... from Goal commands
1998-07-15 paulson 1998-07-15 Removal of leading "\!\!..." from most Goal commands
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-04-27 nipkow 1998-04-27 Added a few lemmas. Renamed expand_const -> split_const.
1998-02-26 paulson 1998-02-26 Proved choice and bchoice; changed Fun.thy -> thy
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-11-01 paulson 1997-11-01 New Blast_tac (and minor tidying...)
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-05-26 paulson 1997-05-26 New theorem subset_inj_onto
1997-04-11 paulson 1997-04-11 Yet more fast_tac->blast_tac, and other tidying
1997-04-09 paulson 1997-04-09 Using Blast_tac
1997-04-04 nipkow 1997-04-04 moved inj and surj from Set to Fun and Inv -> inv.
1997-04-04 paulson 1997-04-04 Adds image_eqI instead of imageI, as the former is more general
1997-01-09 paulson 1997-01-09 Tidying of proofs. New theorems are enterred immediately into the relevant clasets or simpsets.
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-07-26 paulson 1996-07-26 Redefining "range" as a macro
1996-06-28 paulson 1996-06-28 Now set_cs is just taken from !claset
1996-06-21 berghofe 1996-06-21 Replaced occurrence of set_cs by claset_of "Fun" .
1996-05-31 oheimb 1996-05-31 moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML, as there have been unnecessary proofs of anonymous thms, which could not be removed (by name) from the !simpset where necessary. All these thms except singleton_iff were already proved in Set.ML. therefore in Set.ML: New version of singletonE, proof of new thm singleton_iff
1996-05-21 berghofe 1996-05-21 Replaced fast_tac by Fast_tac (which uses default claset) New rules are now also added to default claset.
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 removed assignment of HOL_ss to simpset
1996-03-11 paulson 1996-03-11 set_cs now includes singleton_inject
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-10-04 clasohm 1995-10-04 added local simpsets; removed IOA from 'make test'
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application