lcp [Wed, 01 Dec 1993 13:05:25 +0100] rev 22
HOL/llist/LList_corec_subset1: does not need induction
nipkow [Tue, 30 Nov 1993 17:44:04 +0100] rev 21
added pred: nat=>nat
nipkow [Mon, 29 Nov 1993 18:35:02 +0100] rev 20
changed simpsets
nipkow [Thu, 25 Nov 1993 10:04:02 +0100] rev 19
added "?!x.f(g(x))=x ==> ?!y.g(f(y))=y"
lcp [Fri, 19 Nov 1993 11:36:23 +0100] rev 18
Trivial spacing corrections
clasohm [Tue, 16 Nov 1993 14:14:22 +0100] rev 17
changed use_thy's parameter to exact theory name
lcp [Tue, 09 Nov 1993 16:31:03 +0100] rev 16
Target "test" now depends on examples files
clasohm [Tue, 09 Nov 1993 13:30:13 +0100] rev 15
renamed meson-test.ML to mesontest.ML,
used exact theory names for use_thy
lcp [Tue, 09 Nov 1993 11:08:13 +0100] rev 14
co-induction example courtesy Jacob Frost
nipkow [Wed, 03 Nov 1993 19:02:17 +0100] rev 13
added append "@"
Proved @ associativ