clasohm [Thu, 26 Oct 1995 12:49:02 +0100] rev 1310
removed buggy FTP scripts and replaced them by a script for transfer
to our HTTP server
clasohm [Thu, 26 Oct 1995 11:47:25 +0100] rev 1309
scripts for transfer of HTML files to FTP server
clasohm [Wed, 25 Oct 1995 13:41:45 +0100] rev 1308
removed "duplicate" warning from store_thm_db;
changed place where store_thm_db is called for a theory's axioms
clasohm [Wed, 25 Oct 1995 12:53:53 +0100] rev 1307
added init_html and make_chart
clasohm [Wed, 25 Oct 1995 12:53:24 +0100] rev 1306
added make_chart
nipkow [Wed, 25 Oct 1995 10:49:53 +0100] rev 1305
Removed Old_HOL
paulson [Wed, 25 Oct 1995 10:15:51 +0100] rev 1304
Unused type sequ deleted
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
clasohm [Tue, 24 Oct 1995 14:42:15 +0100] rev 1293
added calls of init_html and make_chart
clasohm [Tue, 24 Oct 1995 13:54:00 +0100] rev 1292
added images for HTML files
clasohm [Tue, 24 Oct 1995 13:53:09 +0100] rev 1291
added generation of HTML files to thy_read.ML;
removed old HTML package
clasohm [Tue, 24 Oct 1995 13:41:06 +0100] rev 1290
added space_explode and relative_path
clasohm [Tue, 24 Oct 1995 13:40:06 +0100] rev 1289
added "execute"
nipkow [Sun, 22 Oct 1995 15:16:57 +0100] rev 1288
Improved a few proofs.
clasohm [Thu, 19 Oct 1995 13:25:03 +0100] rev 1287
corrected spelling of title (to test new CVS loginfo)
regensbu [Tue, 17 Oct 1995 17:59:47 +0100] rev 1286
*** empty log message ***
regensbu [Tue, 17 Oct 1995 17:00:10 +0100] rev 1285
removed incompatibility with sml
regensbu [Tue, 17 Oct 1995 16:53:29 +0100] rev 1284
removed incompatibility with sml
paulson [Tue, 17 Oct 1995 12:09:46 +0100] rev 1283
Documented store_thm and moved qed to top
paulson [Mon, 16 Oct 1995 16:32:56 +0100] rev 1282
Added the new Limit.{thy,ML} example
paulson [Mon, 16 Oct 1995 14:56:24 +0100] rev 1281
The inverse limit construction -- thanks to Sten Agerholm