1998-09-21 oheimb 1998-09-21 added wrapper for bspec
1998-09-15 paulson 1998-09-15 From Compl(A) to -A
1998-09-10 paulson 1998-09-10 Changed equals0E back to equals0D and gave it the correct destruct form
1998-08-19 paulson 1998-08-19 fixed overloading of "image"
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 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-08-06 paulson 1998-08-06 Now recognizes both {}= and ={}
1998-08-05 paulson 1998-08-05 Renamed equals0D to equals0E
1998-08-04 paulson 1998-08-04 Deleted the redundant rule mem_if
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-04-02 paulson 1998-04-02 changed if_bool_eq to if_bool_eq_conj
1998-03-07 nipkow 1998-03-07 Removed `addsplits [expand_if]'
1998-01-08 paulson 1998-01-08 New rule: image_subset
1998-01-02 paulson 1998-01-02 New theorem image_subsetI
1997-12-24 paulson 1997-12-24 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-12-23 paulson 1997-12-23 Overloading info for image
1997-12-18 paulson 1997-12-18 UNIV_I no longer counts as safe
1997-12-16 wenzelm 1997-12-16 expandshort;
1997-11-20 paulson 1997-11-20 Renamed "overload" to "overloaded" for sml/nj compatibility
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-15 nipkow 1997-11-15 Added > "(? x : f `` A. P x) = (? a:A. P(f a))" > "(! x : f `` A. P x) = (! a:A. P(f a))"
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_empty and bex_empty (see equalities.ML)
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-11-01 paulson 1997-11-01 New Blast_tac (and minor tidying...)
1997-10-21 paulson 1997-10-21 New rewrite rules image_iff
1997-10-17 nipkow 1997-10-17 setloop split_tac -> addsplits
1997-10-17 paulson 1997-10-17 New rewrite rules for simplifying conditionals
1997-10-17 nipkow 1997-10-17 Added image_eqI to simpset.
1997-10-16 nipkow 1997-10-16 Modified comment.
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-10 wenzelm 1997-10-10 fixed dots;
1997-09-26 paulson 1997-09-26 Minor tidying to use Clarify_tac, etc.
1997-08-01 nipkow 1997-08-01 Added {x.x=a} = a to !simpset.
1997-07-01 paulson 1997-07-01 Now Collect_mem_eq is a default simprule (how could it have ever been omitted?
1997-06-06 paulson 1997-06-06 New miniscoping rules ball_triv and bex_triv
1997-05-16 nipkow 1997-05-16 Distributed Psubset stuff to basic set theory files, incl Finite. Added stuff by bu.
1997-04-11 paulson 1997-04-11 Yet more fast_tac->blast_tac, and other tidying
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-04-03 paulson 1997-04-03 Declares overloading for set-theoretic constants
1997-04-02 paulson 1997-04-02 Re-ordering of rules to assist blast_tac Powerset rules must not be the most recent
1997-03-05 paulson 1997-03-05 New version of InterE, like its ZF counterpart
1997-02-12 nipkow 1997-02-12 New class "order" and accompanying changes. In particular reflexivity of <= is now one rewrite rule.
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-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-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-08-22 paulson 1996-08-22 Proved mem_if
1996-08-19 paulson 1996-08-19 Added impOfSubs
1996-07-26 paulson 1996-07-26 Proved bex_False
1996-06-28 paulson 1996-06-28 Added contra_subsetD and rev_contra_subsetD
1996-06-18 paulson 1996-06-18 New rewrites for vacuous quantification
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-23 berghofe 1996-05-23 equalityI is now added to 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.