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

file  diff  annotate 
19970416 
wenzelm 
19970416 
improved translations for subset symbols syntax: constraints;

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

file  diff  annotate 
19970225 
wenzelm 
19970225 
added proper subset symbols syntax;

file  diff  annotate 
19961216 
wenzelm 
19961216 
fixed \<subseteq> input;

file  diff  annotate 
19961213 
oheimb 
19961213 
adaptions for symbol font

file  diff  annotate 
19961213 
wenzelm 
19961213 
added set inclusion symbol syntax;

file  diff  annotate 
19961210 
wenzelm 
19961210 
fixed alternative quantifier symbol syntax;

file  diff  annotate 
19961210 
wenzelm 
19961210 
fixed pris of binder syntax;

file  diff  annotate 
19961127 
wenzelm 
19961127 
added "op :", "op ~:" syntax;
added symbols syntax;

file  diff  annotate 
19960923 
paulson 
19960923 
New infix syntax: breaks line BEFORE operator

file  diff  annotate 
19960909 
paulson 
19960909 
Corrected associativity: must be to right, as the type dictatess

file  diff  annotate 
19960726 
paulson 
19960726 
Redefining "range" as a macro

file  diff  annotate 
19960423 
oheimb 
19960423 
*** empty log message ***

file  diff  annotate 
19960423 
oheimb 
19960423 
repaired critical proofs depending on the order inside nonconfluent SimpSets,
(temporarily) removed problematic rule less_Suc_eq form simpset_of "Nat"

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 
19951129 
clasohm 
19951129 
removed quotes from types in consts and syntax sections

file  diff  annotate 
19951006 
regensbu 
19951006 
added 8bit pragmas

file  diff  annotate 
19950422 
nipkow 
19950422 
HOL.thy:
"@" is no longer introduced as a "binder" but has its own explicit
translation rule "@x.b" == "Eps(%x.b)". If x is a proper pattern, further
translation rules for abstractions with patterns take care of the rest. This
is very modular and avoids problems with "binders" such as "!" mentioned
below.
let now allows pttrn (let (x,y) = t in u) instead of just idt (let x = t in u)
Set.thy:
UN, INT, ALL, EX, etc all use "pttrn" instead of idt. Same change as for "@"
above, except that "@" was a "binder" originally.
Prod.thy:
Added new syntax for pttrn which allows arbitrarily nested tuples. Two
translation rules take care of %pttrn. Unfortunately they cannot be
reversed. Hence a little MLcode is used as well.
Note that now "! (x,y). ..." is syntactically valid but leads to a
translation error. This is because "!" is introduced as a "binder" which
means that its translation into lambdaterms is not done by a rewrite rule
(aka macro) but by some fixed MLcode which comes after the rewriting stage
and does not know how to handle patterns. This looks like a minor blemish
since patterns in unbounded quantifiers are not that useful (well, except
maybe in unique existence ...). Ideally, there should be two syntactic
categories:
idts, as we know and love it, which does not admit patterns.
patterns, which is what idts has become now.
There is one more point where patterns are now allowed but don't make sense:
{e  idts . P}
where idts is the list of local variables.
Univ.thy: converted the defs for <++> and <**> into pattern form. It worked
perfectly.

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

file  diff  annotate 