| Mon, 07 Mar 2005 19:17:07 +0100 |
webertj |
HTML 4.01 Transitional conformity
|
changeset |
files
|
| Mon, 07 Mar 2005 18:40:36 +0100 |
paulson |
now checks for higher-order vars
|
changeset |
files
|
| Mon, 07 Mar 2005 18:19:55 +0100 |
obua |
Cleaning up HOL/Matrix
|
changeset |
files
|
| Mon, 07 Mar 2005 16:55:36 +0100 |
paulson |
Tools/meson.ML: signature, structure and "open" rather than "local"
|
changeset |
files
|
| Fri, 04 Mar 2005 23:25:06 +0100 |
huffman |
add header
|
changeset |
files
|
| 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
|
| Wed, 23 Feb 2005 14:04:53 +0100 |
webertj |
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
|
changeset |
files
|
| Wed, 23 Feb 2005 10:23:22 +0100 |
nipkow |
suminf -> \<Sum>
|
changeset |
files
|
| Tue, 22 Feb 2005 18:42:22 +0100 |
dixon |
Lucas - fixed bug in zero_var_indexes: it was ignoring vars in the flex-flex pairs. These are now taken into account.
|
changeset |
files
|
| Tue, 22 Feb 2005 13:05:47 +0100 |
paulson |
removed redundant lemmas and simprules
|
changeset |
files
|
| Tue, 22 Feb 2005 10:54:30 +0100 |
nipkow |
more setsum tuning
|
changeset |
files
|
| Mon, 21 Feb 2005 19:23:46 +0100 |
nipkow |
more fine tuniung
|
changeset |
files
|
| Mon, 21 Feb 2005 18:04:28 +0100 |
nipkow |
fixed proof
|
changeset |
files
|
| Mon, 21 Feb 2005 15:57:45 +0100 |
nipkow |
removed superfluous setsum_constant
|
changeset |
files
|
| Mon, 21 Feb 2005 15:04:10 +0100 |
nipkow |
comprehensive cleanup, replacing sumr by setsum
|
changeset |
files
|
| Sat, 19 Feb 2005 18:44:34 +0100 |
dixon |
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
|
changeset |
files
|
| Fri, 18 Feb 2005 15:20:27 +0100 |
nipkow |
continued eliminating sumr
|
changeset |
files
|
| Fri, 18 Feb 2005 11:48:53 +0100 |
nipkow |
starting to get rid of sumr
|
changeset |
files
|
| Fri, 18 Feb 2005 11:48:42 +0100 |
nipkow |
tuning
|
changeset |
files
|
| Wed, 16 Feb 2005 19:00:49 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Tue, 15 Feb 2005 16:56:15 +0100 |
berghofe |
refine now provides specific cases "goal1" ... "goaln" for addressing
|
changeset |
files
|
| Mon, 14 Feb 2005 10:24:58 +0100 |
paulson |
simplified a proof
|
changeset |
files
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
changeset |
files
|
| Fri, 11 Feb 2005 18:51:00 +0100 |
berghofe |
Fully qualified refl and trans to avoid confusion with theorems
|
changeset |
files
|
| Fri, 11 Feb 2005 17:11:24 +0100 |
berghofe |
Optimized present_tokens to produce fewer newlines when hiding proofs.
|
changeset |
files
|
| Fri, 11 Feb 2005 10:03:41 +0100 |
ballarin |
New reference Toplevel.debug for verbose printing of exns.
|
changeset |
files
|
| Fri, 11 Feb 2005 04:36:22 +0100 |
kleing |
update from Larry
|
changeset |
files
|
| Thu, 10 Feb 2005 19:14:35 +0100 |
nipkow |
some stuff is now redundant.
|
changeset |
files
|
| Thu, 10 Feb 2005 18:51:54 +0100 |
nipkow |
HOL.order -> Orderings.order due to restructering
|
changeset |
files
|
| Thu, 10 Feb 2005 18:51:12 +0100 |
nipkow |
Moved oderings from HOL into the new Orderings.thy
|
changeset |
files
|
| Thu, 10 Feb 2005 17:09:15 +0100 |
berghofe |
Added paper by M. Takahashi.
|
changeset |
files
|