19960206 
clasohm 
19960206 
expanded tabs

file  diff  annotate 
19951209 
clasohm 
19951209 
removed quotes from consts and syntax sections

file  diff  annotate 
19950622 
clasohm 
19950622 
removed \...\ inside strings

file  diff  annotate 
19950510 
nipkow 
19950510 
Modified translation for pattern abstraction.

file  diff  annotate 
19950504 
lcp 
19950504 
Added patternmatching code from CHOL/Prod.thy. Changed
definitions so that split is now defined in terms of fst, snd. Now split is
polymorphic. Deleted fsplit, as split(...)::o gives a similar effect  NOT
identical though, as fsplit(P,z) implied that z was a pair, while split(P,z)
means only P(fst(z),snd(z)).

file  diff  annotate 
19941103 
lcp 
19941103 
ZF: NEW DEFINITION OF PI(A,B)
Was Pi(A,B) == {f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f}
Now function(r) == ALL x y. <x,y>:r > (ALL y'. <x,y'>:r > y=y')
Pi(A,B) == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}"
This simplifies many proofs, since (a) the toplevel definition has fewer
bound variables (b) the "total" and "function" properties are separated
(c) the awkward EX! quantifier is eliminated.
ZF/ZF.thy/function: new definition

file  diff  annotate 
19941031 
lcp 
19941031 
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}

file  diff  annotate 
19941012 
wenzelm 
19941012 
fixed infix names in print_translations;

file  diff  annotate 
19940921 
wenzelm 
19940921 
minor cleanup, added 'syntax' section;

file  diff  annotate 
19940812 
lcp 
19940812 
installation of new inductive/datatype sections

file  diff  annotate 
19940726 
lcp 
19940726 
Axiom of choice, cardinality results, etc.

file  diff  annotate 
19940503 
lcp 
19940503 
removal of obsolete typedeclaration syntax

file  diff  annotate 
19931025 
wenzelm 
19931025 
added whitespace;
made ~: a fake infix;

file  diff  annotate 
19931011 
wenzelm 
19931011 
"The" now a binder, removed translation;
improved encoding and translations of tuples;
added parse rules for > and *, removed ndependent_tr;

file  diff  annotate 
19931007 
lcp 
19931007 
added ~: for "not in"

file  diff  annotate 
19930916 
clasohm 
19930916 
Initial revision

file  diff  annotate 