19950509 
nipkow 
19950509 
Prod is now a parent of Lfp.
Added thm induct2 to Lfp.
Changed the way patterns in abstractions are pretty printed.
It has become simpler now but fails if split has more than one argument
because then the asttranslation does not match.

file  diff  annotate 
19950503 
nipkow 
19950503 
Corrected display of split f t: no more let.
Also replaced "_abs" by "_lambda"  the former was a mistake which
happended to work.

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 
19950324 
clasohm 
19950324 
changed syntax of tuples from <..., ...> to (..., ...)

file  diff  annotate 
19950321 
clasohm 
19950321 
changed syntax of Unity ("()" instead of "<>")

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

file  diff  annotate 