19961213 
oheimb 
19961213 
adaptions for symbol font

file  diff  annotate 
19961127 
wenzelm 
19961127 
added symbols syntax;

file  diff  annotate 
19960524 
nipkow 
19960524 
Removed junk introduced by a cvs merge.

file  diff  annotate 
19960521 
berghofe 
19960521 
Added additional parent theory equalities because some proofs in
Prod.ML depend on rules proved in equalities.ML

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 
19960417 
oheimb 
19960417 
*** empty log message ***

file  diff  annotate 
19960411 
nipkow 
19960411 
Added a number of lemmas

file  diff  annotate 
19960403 
nipkow 
19960403 
Introduced Times and SIGMA.

file  diff  annotate 
19960308 
clasohm 
19960308 
added constdefs section

file  diff  annotate 
19960205 
clasohm 
19960205 
expanded tabs; renamed subtype to typedef;
incorporated Konrad's changes

file  diff  annotate 
19960126 
nipkow 
19960126 
Streamlined defs in Relation and added new intro/elim rules to do with
pattern matching in sets: {(x,y). ...} and UN (x,y):A. ...

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 
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 