19980108 
paulson 
19980108 
New rule: image_subset

file  diff  annotate 
19980102 
paulson 
19980102 
New theorem image_subsetI

file  diff  annotate 
19971224 
paulson 
19971224 
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort

file  diff  annotate 
19971223 
paulson 
19971223 
Overloading info for image

file  diff  annotate 
19971218 
paulson 
19971218 
UNIV_I no longer counts as safe

file  diff  annotate 
19971216 
wenzelm 
19971216 
expandshort;

file  diff  annotate 
19971120 
paulson 
19971120 
Renamed "overload" to "overloaded" for sml/nj compatibility

file  diff  annotate 
19971116 
nipkow 
19971116 
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.

file  diff  annotate 
19971115 
nipkow 
19971115 
Added
> "(? x : f `` A. P x) = (? a:A. P(f a))"
> "(! x : f `` A. P x) = (! a:A. P(f a))"

file  diff  annotate 
19971105 
paulson 
19971105 
UNIV now a constant; UNION1, INTER1 now translations and no longer have
separate rules for themselves

file  diff  annotate 
19971104 
oheimb 
19971104 
removed redundant ball_empty and bex_empty (see equalities.ML)

file  diff  annotate 
19971103 
wenzelm 
19971103 
isatool fixclasimp;

file  diff  annotate 
19971101 
paulson 
19971101 
New Blast_tac (and minor tidying...)

file  diff  annotate 
19971021 
paulson 
19971021 
New rewrite rules image_iff

file  diff  annotate 
19971017 
nipkow 
19971017 
setloop split_tac > addsplits

file  diff  annotate 
19971017 
paulson 
19971017 
New rewrite rules for simplifying conditionals

file  diff  annotate 
19971017 
nipkow 
19971017 
Added image_eqI to simpset.

file  diff  annotate 
19971016 
nipkow 
19971016 
Modified comment.

file  diff  annotate 
19971016 
nipkow 
19971016 
Various new lemmas. Improved conversion of equations to rewrite rules:
(s=t becomes (s=t)==True if s=t loops).

file  diff  annotate 
19971010 
wenzelm 
19971010 
fixed dots;

file  diff  annotate 
19970926 
paulson 
19970926 
Minor tidying to use Clarify_tac, etc.

file  diff  annotate 
19970801 
nipkow 
19970801 
Added {x.x=a} = a to !simpset.

file  diff  annotate 
19970701 
paulson 
19970701 
Now Collect_mem_eq is a default simprule (how could it have ever been omitted?

file  diff  annotate 
19970606 
paulson 
19970606 
New miniscoping rules ball_triv and bex_triv

file  diff  annotate 
19970516 
nipkow 
19970516 
Distributed Psubset stuff to basic set theory files, incl Finite.
Added stuff by bu.

file  diff  annotate 
19970411 
paulson 
19970411 
Yet more fast_tac>blast_tac, and other tidying

file  diff  annotate 
19970404 
nipkow 
19970404 
moved inj and surj from Set to Fun and Inv > inv.

file  diff  annotate 
19970404 
paulson 
19970404 
Calls Blast_tac

file  diff  annotate 
19970403 
paulson 
19970403 
Declares overloading for settheoretic constants

file  diff  annotate 
19970402 
paulson 
19970402 
Reordering of rules to assist blast_tac
Powerset rules must not be the most recent

file  diff  annotate 
19970305 
paulson 
19970305 
New version of InterE, like its ZF counterpart

file  diff  annotate 
19970212 
nipkow 
19970212 
New class "order" and accompanying changes.
In particular reflexivity of <= is now one rewrite rule.

file  diff  annotate 
19970109 
paulson 
19970109 
Tidying of proofs. New theorems are enterred immediately into the
relevant clasets or simpsets.

file  diff  annotate 
19960926 
paulson 
19960926 
Ran expandshort

file  diff  annotate 
19960925 
paulson 
19960925 
Rationalized the rewriting of membership for {} and insert
by deleting the redundant theorems in_empty and in_insert

file  diff  annotate 
19960912 
paulson 
19960912 
Tidied many proofs, using AddIffs to let equivalences take
the place of separate Intr and Elim rules. Also deleted most named clasets.

file  diff  annotate 
19960822 
paulson 
19960822 
Proved mem_if

file  diff  annotate 
19960819 
paulson 
19960819 
Added impOfSubs

file  diff  annotate 
19960726 
paulson 
19960726 
Proved bex_False

file  diff  annotate 
19960628 
paulson 
19960628 
Added contra_subsetD and rev_contra_subsetD

file  diff  annotate 
19960618 
paulson 
19960618 
New rewrites for vacuous quantification

file  diff  annotate 
19960531 
oheimb 
19960531 
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

file  diff  annotate 
19960523 
berghofe 
19960523 
equalityI is now added to default claset

file  diff  annotate 
19960523 
berghofe 
19960523 
Replaced fast_tac by Fast_tac (which uses default claset)
New rules are now also added to default claset.

file  diff  annotate 
19960404 
paulson 
19960404 
Added more _iff rewrites for Compl, Un, Int

file  diff  annotate 
19960327 
paulson 
19960327 
Library changes for mutilated checkerboard

file  diff  annotate 
19960306 
paulson 
19960306 
Ran expandshort

file  diff  annotate 
19960306 
nipkow 
19960306 
Added 'section' commands

file  diff  annotate 
19960304 
nipkow 
19960304 
Added a constant UNIV == {x.True}
Added many new rewrite rules for sets.
Moved LEAST into Nat.
Added cardinality to Finite.

file  diff  annotate 
19960130 
clasohm 
19960130 
expanded tabs

file  diff  annotate 
19950303 
clasohm 
19950303 
new version of HOL with curried function application

file  diff  annotate 