src/HOL/equalities.ML
1998-08-06 paulson 1998-08-06 even more tidying of Goal commands
1998-08-04 paulson 1998-08-04 Boolean quantification
1998-08-03 paulson 1998-08-03 New rewrite rules for quantification over bounded UNIONs
1998-07-24 berghofe 1998-07-24 Added theorem distinct_lemma (needed for 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-05-01 oheimb 1998-05-01 added insert_Collect
1998-04-02 paulson 1998-04-02 new theorems
1998-03-23 paulson 1998-03-23 more thms
1998-03-07 nipkow 1998-03-07 Removed `addsplits [expand_if]'
1998-03-03 paulson 1998-03-03 New theorems
1998-02-27 paulson 1998-02-27 New absorbsion laws, etc
1998-02-23 paulson 1998-02-23 New laws for union
1998-02-19 paulson 1998-02-19 Four new Union/Intersection laws
1998-02-10 paulson 1998-02-10 New Addsimps for Compl rules
1998-02-07 paulson 1998-02-07 AC and other rewrite rules for Un and Int
1998-02-06 nipkow 1998-02-06 Added `remdups' nodup -> nodups
1997-12-24 paulson 1997-12-24 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-12-16 wenzelm 1997-12-16 expandshort;
1997-11-26 paulson 1997-11-26 Tidying and using equalityCE instead of the slower equalityE
1997-11-16 nipkow 1997-11-16 Removed "(ALL x:f``A. P x) = (ALL x:A. P(f x))", "(EX x:f``A. P x) = (EX x:A. P(f x))", again, because they were already there and added "(UN x:f``A. B x) = (UN a:A. B(f a))" "(INT x:f``A. B x) = (INT a:A. B(f a))" instead.
1997-11-11 paulson 1997-11-11 Rationalized the theorem if_image_distrib. Added parens to not_empty.
1997-11-10 oheimb 1997-11-10 replaced 8bit characters
1997-11-05 paulson 1997-11-05 UNIV now a constant; UNION1, INTER1 now translations and no longer have separate rules for themselves
1997-11-04 oheimb 1997-11-04 removed redundant ball_image added image_cong and not_empty added ball and bex of UNIV
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-11-01 paulson 1997-11-01 New Blast_tac (and minor tidying...)
1997-10-24 nipkow 1997-10-24 Added goal Set.thy "(Union M = {}) = (! A : M. A = {})"; AddIffs [Union_empty_conv]; Good idea??
1997-10-17 nipkow 1997-10-17 setloop split_tac -> addsplits
1997-10-16 nipkow 1997-10-16 AddIffs [all_not_in_conv];
1997-10-16 nipkow 1997-10-16 Various new lemmas. Improved conversion of equations to rewrite rules: (s=t becomes (s=t)==True if s=t loops).
1997-10-14 nipkow 1997-10-14 More lemmas, esp. ~Bex and ~Ball conversions.
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-09-29 paulson 1997-09-29 Step_tac -> Safe_tac
1997-06-23 paulson 1997-06-23 Ran expandshort
1997-06-06 paulson 1997-06-06 The name bex_conj_distrib was WRONG
1997-06-06 paulson 1997-06-06 New miniscoping rules for ALL
1997-06-05 nipkow 1997-06-05 Moved image_is_empty from Finite.ML to equalities.ML
1997-06-02 paulson 1997-06-02 Now Un_insert_left, Un_insert_right are default rewrite rules
1997-05-27 paulson 1997-05-27 New theorem disjoint_eq_subset_Compl
1997-05-26 paulson 1997-05-26 Two useful facts about Powersets suggested by Florian Kammueller
1997-05-16 nipkow 1997-05-16 Distributed Psubset stuff to basic set theory files, incl Finite. Added stuff by bu.
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 Calls Blast_tac
1997-01-17 paulson 1997-01-17 New rewrites for bounded quantifiers
1997-01-17 paulson 1997-01-17 New miniscoping rules for the bounded quantifiers and UN/INT operators
1997-01-17 nipkow 1997-01-17 Got rid of Alls in List. Added Ball_insert and Ball_Un in equalities.ML.
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-09-25 paulson 1996-09-25 Rationalized the rewriting of membership for {} and insert by deleting the redundant theorems in_empty and in_insert
1996-09-24 paulson 1996-09-24 Added miniscoping for UN and INT
1996-08-19 paulson 1996-08-19 Added proof of Un_insert_right
1996-07-26 paulson 1996-07-26 Proved insert_image
1996-07-22 paulson 1996-07-22 Added insert_commute
1996-06-28 paulson 1996-06-28 Removed the unused eq_cs, and added some distributive laws
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 expanded TABs
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-05-17 nipkow 1996-05-17 Added if_image_distrib.