clasohm [Mon, 05 Feb 1996 21:27:16 +0100] rev 1475
expanded tabs; renamed subtype to typedef;
incorporated Konrad's changes
clasohm [Mon, 05 Feb 1996 14:44:09 +0100] rev 1474
expanded tabs
clasohm [Mon, 05 Feb 1996 13:44:28 +0100] rev 1473
expanded tabs
clasohm [Fri, 02 Feb 1996 12:05:24 +0100] rev 1472
renamed subtype.ML to typedef.ML
nipkow [Thu, 01 Feb 1996 16:18:52 +0100] rev 1471
documented split_all_tac in HOL.
clasohm [Thu, 01 Feb 1996 13:25:40 +0100] rev 1470
renamed subtype.ML to typedef.ML
clasohm [Thu, 01 Feb 1996 12:08:43 +0100] rev 1469
fixed two little bugs
nipkow [Wed, 31 Jan 1996 17:15:03 +0100] rev 1468
right-hard -> right-hand
nipkow [Wed, 31 Jan 1996 15:02:26 +0100] rev 1467
Typo
clasohm [Tue, 30 Jan 1996 15:31:04 +0100] rev 1466
fixed typo
clasohm [Tue, 30 Jan 1996 15:24:36 +0100] rev 1465
expanded tabs
clasohm [Tue, 30 Jan 1996 15:19:20 +0100] rev 1464
expanded tabs; removed commit() from ROOT.ML
clasohm [Tue, 30 Jan 1996 15:12:53 +0100] rev 1463
expanded tabs
clasohm [Tue, 30 Jan 1996 13:56:16 +0100] rev 1462
fixed typo
clasohm [Tue, 30 Jan 1996 13:42:57 +0100] rev 1461
expanded tabs
clasohm [Mon, 29 Jan 1996 14:16:13 +0100] rev 1460
inserted tabs again
clasohm [Mon, 29 Jan 1996 13:58:15 +0100] rev 1459
expanded tabs
clasohm [Mon, 29 Jan 1996 13:56:41 +0100] rev 1458
removed tabs
clasohm [Mon, 29 Jan 1996 13:50:10 +0100] rev 1457
added facility to associate arbitrary data with theories
clasohm [Mon, 29 Jan 1996 13:49:17 +0100] rev 1456
added absolute_path
clasohm [Mon, 29 Jan 1996 13:48:37 +0100] rev 1455
changed the way simpsets and information about datatypes are stored
nipkow [Fri, 26 Jan 1996 20:25:39 +0100] rev 1454
Streamlined defs in Relation and added new intro/elim rules to do with
pattern matching in sets: {(x,y). ...} and UN (x,y):A. ...
clasohm [Fri, 26 Jan 1996 13:43:36 +0100] rev 1453
extended warning regarding MAKE_HTML databases
clasohm [Fri, 26 Jan 1996 12:45:09 +0100] rev 1452
added warning for databases made with set MAKE_HTML
nipkow [Tue, 23 Jan 1996 14:25:55 +0100] rev 1451
Added vcwp
paulson [Tue, 23 Jan 1996 11:33:46 +0100] rev 1450
Renamed letI to LetI (for consistency)
paulson [Tue, 23 Jan 1996 11:27:29 +0100] rev 1449
Added discussion of "let" and pattern-matching
paulson [Tue, 23 Jan 1996 11:10:39 +0100] rev 1448
Stylistic changes to discussion of pattern-matching
nipkow [Tue, 23 Jan 1996 10:59:35 +0100] rev 1447
Added a verified verification-condition generator.
paulson [Sat, 20 Jan 1996 02:00:11 +0100] rev 1446
Ran expandshort
paulson [Fri, 19 Jan 1996 16:00:22 +0100] rev 1445
Now expands TABS as well
paulson [Thu, 18 Jan 1996 10:38:29 +0100] rev 1444
trivial updates
paulson [Thu, 18 Jan 1996 10:28:20 +0100] rev 1443
New version number
wenzelm [Mon, 15 Jan 1996 15:50:54 +0100] rev 1442
*** empty log message ***
wenzelm [Mon, 15 Jan 1996 15:50:41 +0100] rev 1441
added Lattice demo;
wenzelm [Mon, 15 Jan 1996 15:49:21 +0100] rev 1440
added this stuff;
wenzelm [Mon, 15 Jan 1996 15:47:10 +0100] rev 1439
improved printing of errors in 'defs';
fixed small bug in 'standard' (it used to fail stripping shyps in some cases);
clasohm [Mon, 15 Jan 1996 15:00:14 +0100] rev 1438
added comments
clasohm [Mon, 15 Jan 1996 14:56:38 +0100] rev 1437
beautified file_info a bit
clasohm [Mon, 15 Jan 1996 14:47:56 +0100] rev 1436
fixed bug in file_info
nipkow [Thu, 11 Jan 1996 10:29:31 +0100] rev 1435
Removed bug in type unification. Negative indexes are not used any longer.
Had to change interface to Type.unify to pass maxidx. Thus changes in the
clients.
clasohm [Tue, 09 Jan 1996 13:45:58 +0100] rev 1434
simplified file_info by using System.filedate
nipkow [Sat, 06 Jan 1996 14:04:12 +0100] rev 1433
removed reference to Nat thms in elim_rls.
nipkow [Sat, 06 Jan 1996 14:02:52 +0100] rev 1432
Minor mod.
nipkow [Tue, 02 Jan 1996 14:08:04 +0100] rev 1431
Polished proofs.
paulson [Tue, 02 Jan 1996 10:46:50 +0100] rev 1430
Improving space efficiency of inductive/datatype definitions.
Reduce usage of "open" and change struct open X; D end to
let open X in struct D end end whenever possible -- removes X from the final
structure. Especially needed for functors Intr_elim and Indrule.
nipkow [Mon, 01 Jan 1996 11:54:36 +0100] rev 1429
Modified non-empty-types warning in HOL.
paulson [Thu, 28 Dec 1995 12:37:57 +0100] rev 1428
Reduced indentation; no change in function
paulson [Thu, 28 Dec 1995 12:37:00 +0100] rev 1427
Purely cosmetic changes
paulson [Thu, 28 Dec 1995 12:36:05 +0100] rev 1426
Updated comments for compression functions
paulson [Thu, 28 Dec 1995 11:59:40 +0100] rev 1425
Removed unfold:thm from signature INTR_ELIM and from the
functor result. It is never used outside, is easily recovered using
bnd_mono and def_lfp_Tarski, and takes up considerable store.
paulson [Thu, 28 Dec 1995 11:59:15 +0100] rev 1424
Now mutual_induct is simply "True" unless it is going to be
significantly different from induct -- either because there is mutual
recursion or because it involves tuples.
paulson [Thu, 28 Dec 1995 11:54:15 +0100] rev 1423
fixed indentation
nipkow [Sat, 23 Dec 1995 12:50:53 +0100] rev 1422
New version of type sections and many small changes.
paulson [Fri, 22 Dec 1995 13:38:57 +0100] rev 1421
Note that unfold is not exported, that mutual_induct can
be omitted (as the trivial theorem True), and comments on storage
Also uses Datatype instead of Univ/Quniv as parent theory for lists, and
omits quotes around types in theory files.
paulson [Fri, 22 Dec 1995 13:33:40 +0100] rev 1420
Added line breaks and other cosmetic changes