Mon, 15 Jan 1996 15:00:14 +0100 added comments
clasohm [Mon, 15 Jan 1996 15:00:14 +0100] rev 1438
added comments
Mon, 15 Jan 1996 14:56:38 +0100 beautified file_info a bit
clasohm [Mon, 15 Jan 1996 14:56:38 +0100] rev 1437
beautified file_info a bit
Mon, 15 Jan 1996 14:47:56 +0100 fixed bug in file_info
clasohm [Mon, 15 Jan 1996 14:47:56 +0100] rev 1436
fixed bug in file_info
Thu, 11 Jan 1996 10:29:31 +0100 Removed bug in type unification. Negative indexes are not used any longer.
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.
Tue, 09 Jan 1996 13:45:58 +0100 simplified file_info by using System.filedate
clasohm [Tue, 09 Jan 1996 13:45:58 +0100] rev 1434
simplified file_info by using System.filedate
Sat, 06 Jan 1996 14:04:12 +0100 removed reference to Nat thms in elim_rls.
nipkow [Sat, 06 Jan 1996 14:04:12 +0100] rev 1433
removed reference to Nat thms in elim_rls.
Sat, 06 Jan 1996 14:02:52 +0100 Minor mod.
nipkow [Sat, 06 Jan 1996 14:02:52 +0100] rev 1432
Minor mod.
Tue, 02 Jan 1996 14:08:04 +0100 Polished proofs.
nipkow [Tue, 02 Jan 1996 14:08:04 +0100] rev 1431
Polished proofs.
Tue, 02 Jan 1996 10:46:50 +0100 Improving space efficiency of inductive/datatype definitions.
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.
Mon, 01 Jan 1996 11:54:36 +0100 Modified non-empty-types warning in HOL.
nipkow [Mon, 01 Jan 1996 11:54:36 +0100] rev 1429
Modified non-empty-types warning in HOL.
(0) -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip