src/HOL/Univ.ML
2000-06-22 wenzelm 2000-06-22 bind_thm(s);
2000-05-04 paulson 2000-05-04 Suc 0 -> 1
2000-04-13 paulson 2000-04-13 stopped using the obsolete "nat_ind_tac"
2000-04-13 nipkow 2000-04-13 Times -> <*> ** -> <*lex*>
2000-02-24 wenzelm 2000-02-24 workaround res_inst_tac/lift_inst_rule bug by explicit type contraint;
2000-01-07 paulson 2000-01-07 tidied parentheses
1999-08-18 berghofe 1999-08-18 Eliminated some infixes.
1999-07-27 paulson 1999-07-27 expandshort; tidied
1999-07-16 berghofe 1999-07-16 Added some definitions and theorems needed for the construction of datatypes involving function types.
1999-02-03 paulson 1999-02-03 inj is now a translation of inj_on
1998-11-27 paulson 1998-11-27 moved diag (diagonal relation) from Univ to Relation
1998-11-09 paulson 1998-11-09 removed obsolete comment and "open" declaration
1998-11-02 paulson 1998-11-02 Domain r, Range r replace fst``r, snd``r
1998-08-13 paulson 1998-08-13 even more tidying of Goal commands
1998-08-06 paulson 1998-08-06 even more tidying of Goal commands
1998-07-24 berghofe 1998-07-24 Renamed '$' to 'Scons' because of clashes with constants of the same name in theories using datatypes.
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-01-08 oheimb 1998-01-08 added select_equality to the implicit claset
1998-01-08 paulson 1998-01-08 Tidied by adding more default simprules
1997-12-03 nipkow 1997-12-03 Replaced n ~= 0 by 0 < n
1997-11-05 paulson 1997-11-05 Ran expandshort, especially to introduce Safe_tac
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-06-06 paulson 1997-06-06 Removed a few redundant additions of simprules or classical rules
1997-06-06 paulson 1997-06-06 New facts about In0/1 by Burkhart Wolff
1997-04-15 paulson 1997-04-15 Removed "AddSDs [Scons_inject];" because (a) IT WAS WRONG (should have been AddSEs) (b) It was redundant (due to the AddIffs [...,Scons_Scons_eq])
1997-04-11 paulson 1997-04-11 Yet more fast_tac->blast_tac, and other tidying
1997-04-04 paulson 1997-04-04 Calls Blast_tac
1996-09-12 paulson 1996-09-12 Tidied many proofs, using AddIffs to let equivalences take the place of separate Intr and Elim rules. Also deleted most named clasets.
1996-06-03 berghofe 1996-06-03 best_tac, deepen_tac and safe_tac now also use default claset.
1996-05-23 berghofe 1996-05-23 Removed equalityI from some proofs (because it is now included in the default claset)
1996-05-23 berghofe 1996-05-23 Replaced fast_tac by Fast_tac (which uses default claset) New rules are now also added to default claset.
1996-04-04 paulson 1996-04-04 Using new "Times" infix
1996-03-11 paulson 1996-03-11 New, one-line proof of inj_Atom
1996-03-04 nipkow 1996-03-04 Added a constant UNIV == {x.True} Added many new rewrite rules for sets. Moved LEAST into Nat. Added cardinality to Finite.
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
1995-10-04 clasohm 1995-10-04 added local simpsets; removed IOA from 'make test'
1995-03-28 clasohm 1995-03-28 renamed theorem "apfst" to "apfst_conv" to avoid conflict with function apfst from Pure/library.ML
1995-03-24 clasohm 1995-03-24 changed syntax of tuples from <..., ...> to (..., ...)
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application