Tue, 23 Jan 1996 11:10:39 +0100 Stylistic changes to discussion of pattern-matching
paulson [Tue, 23 Jan 1996 11:10:39 +0100] rev 1448
Stylistic changes to discussion of pattern-matching
Tue, 23 Jan 1996 10:59:35 +0100 Added a verified verification-condition generator.
nipkow [Tue, 23 Jan 1996 10:59:35 +0100] rev 1447
Added a verified verification-condition generator.
Sat, 20 Jan 1996 02:00:11 +0100 Ran expandshort
paulson [Sat, 20 Jan 1996 02:00:11 +0100] rev 1446
Ran expandshort
Fri, 19 Jan 1996 16:00:22 +0100 Now expands TABS as well
paulson [Fri, 19 Jan 1996 16:00:22 +0100] rev 1445
Now expands TABS as well
Thu, 18 Jan 1996 10:38:29 +0100 trivial updates Isabelle94-5
paulson [Thu, 18 Jan 1996 10:38:29 +0100] rev 1444
trivial updates
Thu, 18 Jan 1996 10:28:20 +0100 New version number
paulson [Thu, 18 Jan 1996 10:28:20 +0100] rev 1443
New version number
Mon, 15 Jan 1996 15:50:54 +0100 *** empty log message ***
wenzelm [Mon, 15 Jan 1996 15:50:54 +0100] rev 1442
*** empty log message ***
Mon, 15 Jan 1996 15:50:41 +0100 added Lattice demo;
wenzelm [Mon, 15 Jan 1996 15:50:41 +0100] rev 1441
added Lattice demo;
Mon, 15 Jan 1996 15:49:21 +0100 added this stuff;
wenzelm [Mon, 15 Jan 1996 15:49:21 +0100] rev 1440
added this stuff;
Mon, 15 Jan 1996 15:47:10 +0100 improved printing of errors in 'defs';
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);
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.
Thu, 28 Dec 1995 12:37:57 +0100 Reduced indentation; no change in function
paulson [Thu, 28 Dec 1995 12:37:57 +0100] rev 1428
Reduced indentation; no change in function
Thu, 28 Dec 1995 12:37:00 +0100 Purely cosmetic changes
paulson [Thu, 28 Dec 1995 12:37:00 +0100] rev 1427
Purely cosmetic changes
Thu, 28 Dec 1995 12:36:05 +0100 Updated comments for compression functions
paulson [Thu, 28 Dec 1995 12:36:05 +0100] rev 1426
Updated comments for compression functions
Thu, 28 Dec 1995 11:59:40 +0100 Removed unfold:thm from signature INTR_ELIM and from the
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.
Thu, 28 Dec 1995 11:59:15 +0100 Now mutual_induct is simply "True" unless it is going to be
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.
Thu, 28 Dec 1995 11:54:15 +0100 fixed indentation
paulson [Thu, 28 Dec 1995 11:54:15 +0100] rev 1423
fixed indentation
Sat, 23 Dec 1995 12:50:53 +0100 New version of type sections and many small changes.
nipkow [Sat, 23 Dec 1995 12:50:53 +0100] rev 1422
New version of type sections and many small changes.
Fri, 22 Dec 1995 13:38:57 +0100 Note that unfold is not exported, that mutual_induct can
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.
Fri, 22 Dec 1995 13:33:40 +0100 Added line breaks and other cosmetic changes
paulson [Fri, 22 Dec 1995 13:33:40 +0100] rev 1420
Added line breaks and other cosmetic changes
Fri, 22 Dec 1995 12:25:20 +0100 defined take/drop by induction over list rather than nat.
nipkow [Fri, 22 Dec 1995 12:25:20 +0100] rev 1419
defined take/drop by induction over list rather than nat.
(0) -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip