| 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
|
| Thu, 10 Feb 2005 17:08:45 +0100 |
berghofe |
Added proof of eta-postponement theorem (using parallel eta-reduction).
|
changeset |
files
|
| Thu, 10 Feb 2005 16:03:18 +0100 |
paulson |
non-inductive fold1Set proofs
|
changeset |
files
|
| Thu, 10 Feb 2005 13:01:46 +0100 |
paulson |
simplified a key lemma for foldSet
|
changeset |
files
|
| Thu, 10 Feb 2005 12:06:40 +0100 |
ballarin |
Toplevel.debug for debugging in Isar.
|
changeset |
files
|
| Thu, 10 Feb 2005 11:19:03 +0100 |
berghofe |
Fixed bug in select_thm.
|
changeset |
files
|
| Thu, 10 Feb 2005 10:43:57 +0100 |
berghofe |
Subscripts for theorem lists now start at 1.
|
changeset |
files
|
| Thu, 10 Feb 2005 08:25:22 +0100 |
kleing |
mention authors are acknowledged for isabelle-lemmas
|
changeset |
files
|
| Thu, 10 Feb 2005 08:21:40 +0100 |
kleing |
more preview
|
changeset |
files
|
| Thu, 10 Feb 2005 07:47:06 +0100 |
kleing |
pointer to isabelle-lemmas submission list
|
changeset |
files
|
| Wed, 09 Feb 2005 18:51:02 +0100 |
nipkow |
added lattice_locales
|
changeset |
files
|
| Wed, 09 Feb 2005 18:50:09 +0100 |
nipkow |
Extracted generic lattice stuff to new Lattice_Locales.thy
|
changeset |
files
|
| Wed, 09 Feb 2005 18:49:29 +0100 |
nipkow |
New
|
changeset |
files
|
| Wed, 09 Feb 2005 18:32:28 +0100 |
paulson |
new foldSet proofs
|
changeset |
files
|
| Wed, 09 Feb 2005 12:08:46 +0100 |
paulson |
revised fold1 proofs
|
changeset |
files
|
| Wed, 09 Feb 2005 10:17:09 +0100 |
paulson |
revised fold1 proofs
|
changeset |
files
|
| Tue, 08 Feb 2005 18:32:34 +0100 |
nipkow |
cvs merge problem fixed
|
changeset |
files
|
| Tue, 08 Feb 2005 15:11:30 +0100 |
paulson |
new treatment of fold1
|
changeset |
files
|
| Tue, 08 Feb 2005 09:46:00 +0100 |
nipkow |
Fixed lattice defns
|
changeset |
files
|
| Mon, 07 Feb 2005 18:20:46 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|