src/HOL/equalities.ML
1998-12-02 paulson 1998-12-02 new theorem Pow_UNIV
1998-12-01 paulson 1998-12-01 new theorem INT_Un
1998-11-25 paulson 1998-11-25 image_id in simpset
1998-11-20 paulson 1998-11-20 better miniscoping rules: the premise C~={} is not good because Safe_tac eliminates such assumptions.
1998-11-18 paulson 1998-11-18 Finally removing "Compl" from HOL
1998-11-13 paulson 1998-11-13 moved UNION_o to Fun.ML, since Fun.thy is no longer a parent of equalities
1998-10-23 berghofe 1998-10-23 Added theorem bool_induct (for rep_datatype).
1998-10-09 paulson 1998-10-09 new theorem
1998-10-01 paulson 1998-10-01 white space
1998-09-21 oheimb 1998-09-21 added wrapper for bspec
1998-09-15 paulson 1998-09-15 From Compl(A) to -A
1998-08-18 paulson 1998-08-18 new theorem Un_Diff_Int
1998-08-14 paulson 1998-08-14 Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
1998-08-13 paulson 1998-08-13 even more tidying of Goal commands
1998-08-08 nipkow 1998-08-08 List now contains some lexicographic orderings.
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.