| Fri, 04 Mar 2005 23:23:47 +0100 |
huffman |
fix headers
|
changeset |
files
|
| Fri, 04 Mar 2005 23:12:36 +0100 |
huffman |
converted to new-style theories, and combined numbered files
|
changeset |
files
|
| Fri, 04 Mar 2005 18:53:46 +0100 |
huffman |
document generation for HOLCF
|
changeset |
files
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
changeset |
files
|
| Fri, 04 Mar 2005 11:44:26 +0100 |
paulson |
new first_order test
|
changeset |
files
|
| Fri, 04 Mar 2005 10:58:04 +0100 |
paulson |
removed dead code
|
changeset |
files
|
| Thu, 03 Mar 2005 17:22:46 +0100 |
webertj |
interpreter for Finite_Set.Finites added
|
changeset |
files
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
changeset |
files
|
| Thu, 03 Mar 2005 09:22:35 +0100 |
nipkow |
fixed proof
|
changeset |
files
|
| Thu, 03 Mar 2005 01:37:32 +0100 |
huffman |
converted to new-style theory
|
changeset |
files
|
| Thu, 03 Mar 2005 00:42:04 +0100 |
huffman |
converted to new-style theory
|
changeset |
files
|
| Wed, 02 Mar 2005 23:58:02 +0100 |
huffman |
converted to new-style theory
|
changeset |
files
|
| Wed, 02 Mar 2005 23:28:17 +0100 |
huffman |
converted to new-style theory
|
changeset |
files
|
| Wed, 02 Mar 2005 23:15:16 +0100 |
huffman |
converted to new-style theory
|
changeset |
files
|
| Wed, 02 Mar 2005 22:57:08 +0100 |
huffman |
converted to new-style theory
|
changeset |
files
|
| Wed, 02 Mar 2005 22:30:00 +0100 |
huffman |
converted to new-style theory
|
changeset |
files
|
| Wed, 02 Mar 2005 12:06:15 +0100 |
nipkow |
another reorganization of setsums and intervals
|
changeset |
files
|
| Wed, 02 Mar 2005 10:33:10 +0100 |
dixon |
lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.
|
changeset |
files
|
| Wed, 02 Mar 2005 10:21:17 +0100 |
paulson |
obscured the e-mail address lcp@cl
|
changeset |
files
|
| Wed, 02 Mar 2005 10:02:21 +0100 |
paulson |
new lemmas int_diff_cases
|
changeset |
files
|
| Wed, 02 Mar 2005 00:56:41 +0100 |
huffman |
eliminated deps for removed files
|
changeset |
files
|
| Wed, 02 Mar 2005 00:55:12 +0100 |
huffman |
merged into Discrete.thy
|
changeset |
files
|
| Wed, 02 Mar 2005 00:54:06 +0100 |
huffman |
converted to new-style theory
|
changeset |
files
|
| Tue, 01 Mar 2005 18:48:52 +0100 |
nipkow |
integrated Jeremy's FiniteLib
|
changeset |
files
|
| Tue, 01 Mar 2005 05:44:13 +0100 |
kleing |
spider dogding
|
changeset |
files
|
| Mon, 28 Feb 2005 18:29:55 +0100 |
obua |
added setsum_diff1' which holds in more general cases than setsum_diff1
|
changeset |
files
|
| Mon, 28 Feb 2005 13:10:36 +0100 |
paulson |
unfold theorems for trancl and rtrancl
|
changeset |
files
|
| Sun, 27 Feb 2005 00:00:40 +0100 |
dixon |
lucas - added more comments and an extra type to clarify the code.
|
changeset |
files
|
| Wed, 23 Feb 2005 15:19:00 +0100 |
berghofe |
Modified node_trans to avoid duplication of signature stamps
|
changeset |
files
|
| Wed, 23 Feb 2005 15:00:03 +0100 |
webertj |
exception SAME removed
|
changeset |
files
|