nipkow [Wed, 25 Oct 1995 09:50:18 +0100] rev 1303
Hat to modify a proof because of chaned simpset for Prod.
nipkow [Wed, 25 Oct 1995 09:49:35 +0100] rev 1302
Moved some thms to Arith and to Trancl.
nipkow [Wed, 25 Oct 1995 09:48:29 +0100] rev 1301
Added various thms and tactics.
nipkow [Wed, 25 Oct 1995 09:46:46 +0100] rev 1300
New theory: type inference for let-free MiniML
clasohm [Tue, 24 Oct 1995 15:01:01 +0100] rev 1299
added usage of qed
clasohm [Tue, 24 Oct 1995 14:58:29 +0100] rev 1298
added call of make_chart
clasohm [Tue, 24 Oct 1995 14:58:02 +0100] rev 1297
added calls of init_html and make_chart;
added usage of qed to LK.ML
clasohm [Tue, 24 Oct 1995 14:50:24 +0100] rev 1296
added calls of init_html and make_chart
clasohm [Tue, 24 Oct 1995 14:49:45 +0100] rev 1295
entry page for HTML version of Isabelle's logics
clasohm [Tue, 24 Oct 1995 14:45:35 +0100] rev 1294
added calls of init_html and make_chart;
added usage of qed