nipkow [Wed, 15 Jun 1994 19:28:35 +0200] rev 79
Added set comprehension as a syntactic abbreviation:
{e | x1..xn. P} means {u. ? x1 .. xn. u=e & P}
lcp [Wed, 01 Jun 1994 13:24:54 +0200] rev 78
added test for $ISABELLEBIN=source directory, to
avoid isabelle/Pure being mistaken for bin/Pure
lcp [Wed, 25 May 1994 13:03:19 +0200] rev 77
HOL/Arith: definition of diff now uses pred, not nat_rec
lcp [Wed, 25 May 1994 12:43:50 +0200] rev 76
HOL/equalities: added some identities from ZF/equalities
HOL/equalities/constant_UN: renamed UN1_constant
HOL/equalities/Union_Un_distrib: deleted duplicate!
HOL/equalities/Union_Int_subset: new
lcp [Wed, 25 May 1994 12:25:40 +0200] rev 75
HOL/HOL.ML/notE: tidied
wenzelm [Thu, 19 May 1994 17:07:19 +0200] rev 74
thy reader now initialised by init_thy_reader();
lcp [Fri, 13 May 1994 11:14:20 +0200] rev 73
HOL/Prod/pair_eq: renamed to Pair_fst_snd_eq
lcp [Tue, 03 May 1994 15:48:19 +0200] rev 72
removal of obsolete type-declaration syntax
lcp [Tue, 03 May 1994 11:30:09 +0200] rev 71
removal of obsolete type-declaration syntax
clasohm [Sun, 24 Apr 1994 11:27:38 +0200] rev 70
renamed theory files