Tue, 08 Mar 2005 00:45:58 +0100 huffman fixed variable name
Tue, 08 Mar 2005 00:32:10 +0100 huffman reordered and arranged for document generation, cleaned up some proofs
Tue, 08 Mar 2005 00:28:46 +0100 huffman removed Cprod3_lemma1 and Cprod3_lemma2
Tue, 08 Mar 2005 00:18:22 +0100 huffman reordered and arranged for document generation, cleaned up some proofs
Tue, 08 Mar 2005 00:15:01 +0100 huffman added subsection headings, cleaned up some proofs
Tue, 08 Mar 2005 00:11:49 +0100 huffman reordered and arranged for document generation, cleaned up some proofs
Tue, 08 Mar 2005 00:00:49 +0100 huffman arranged for document generation, cleaned up some proofs
Mon, 07 Mar 2005 23:54:01 +0100 huffman added subsections and text for document generation
Mon, 07 Mar 2005 23:30:06 +0100 huffman Added dependency document/root.tex, and -g true option to isatool; document generation should work now.
Mon, 07 Mar 2005 19:41:04 +0100 webertj HTML 4.01 Transitional conformity
Mon, 07 Mar 2005 19:30:53 +0100 webertj refute_params: default value itself=1 added (for type classes)
Mon, 07 Mar 2005 19:25:13 +0100 webertj HTML 4.01 Transitional conformity
Mon, 07 Mar 2005 19:17:07 +0100 webertj HTML 4.01 Transitional conformity
Mon, 07 Mar 2005 18:40:36 +0100 paulson now checks for higher-order vars
Mon, 07 Mar 2005 18:19:55 +0100 obua Cleaning up HOL/Matrix
Mon, 07 Mar 2005 16:55:36 +0100 paulson Tools/meson.ML: signature, structure and "open" rather than "local"
Fri, 04 Mar 2005 23:25:06 +0100 huffman add header
Fri, 04 Mar 2005 23:23:47 +0100 huffman fix headers
Fri, 04 Mar 2005 23:12:36 +0100 huffman converted to new-style theories, and combined numbered files
Fri, 04 Mar 2005 18:53:46 +0100 huffman document generation for HOLCF
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr.
Fri, 04 Mar 2005 11:44:26 +0100 paulson new first_order test
Fri, 04 Mar 2005 10:58:04 +0100 paulson removed dead code
Thu, 03 Mar 2005 17:22:46 +0100 webertj interpreter for Finite_Set.Finites added
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Thu, 03 Mar 2005 09:22:35 +0100 nipkow fixed proof
Thu, 03 Mar 2005 01:37:32 +0100 huffman converted to new-style theory
Thu, 03 Mar 2005 00:42:04 +0100 huffman converted to new-style theory
Wed, 02 Mar 2005 23:58:02 +0100 huffman converted to new-style theory
Wed, 02 Mar 2005 23:28:17 +0100 huffman converted to new-style theory
Wed, 02 Mar 2005 23:15:16 +0100 huffman converted to new-style theory
Wed, 02 Mar 2005 22:57:08 +0100 huffman converted to new-style theory
Wed, 02 Mar 2005 22:30:00 +0100 huffman converted to new-style theory
Wed, 02 Mar 2005 12:06:15 +0100 nipkow another reorganization of setsums and intervals
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.
Wed, 02 Mar 2005 10:21:17 +0100 paulson obscured the e-mail address lcp@cl
Wed, 02 Mar 2005 10:02:21 +0100 paulson new lemmas int_diff_cases
Wed, 02 Mar 2005 00:56:41 +0100 huffman eliminated deps for removed files
Wed, 02 Mar 2005 00:55:12 +0100 huffman merged into Discrete.thy
Wed, 02 Mar 2005 00:54:06 +0100 huffman converted to new-style theory
Tue, 01 Mar 2005 18:48:52 +0100 nipkow integrated Jeremy's FiniteLib
Tue, 01 Mar 2005 05:44:13 +0100 kleing spider dogding
Mon, 28 Feb 2005 18:29:55 +0100 obua added setsum_diff1' which holds in more general cases than setsum_diff1
Mon, 28 Feb 2005 13:10:36 +0100 paulson unfold theorems for trancl and rtrancl
Sun, 27 Feb 2005 00:00:40 +0100 dixon lucas - added more comments and an extra type to clarify the code.
Wed, 23 Feb 2005 15:19:00 +0100 berghofe Modified node_trans to avoid duplication of signature stamps
Wed, 23 Feb 2005 15:00:03 +0100 webertj exception SAME removed
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
Wed, 23 Feb 2005 10:23:22 +0100 nipkow suminf -> \<Sum>
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.
Tue, 22 Feb 2005 13:05:47 +0100 paulson removed redundant lemmas and simprules
Tue, 22 Feb 2005 10:54:30 +0100 nipkow more setsum tuning
Mon, 21 Feb 2005 19:23:46 +0100 nipkow more fine tuniung
Mon, 21 Feb 2005 18:04:28 +0100 nipkow fixed proof
Mon, 21 Feb 2005 15:57:45 +0100 nipkow removed superfluous setsum_constant
Mon, 21 Feb 2005 15:04:10 +0100 nipkow comprehensive cleanup, replacing sumr by setsum
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.
Fri, 18 Feb 2005 15:20:27 +0100 nipkow continued eliminating sumr
Fri, 18 Feb 2005 11:48:53 +0100 nipkow starting to get rid of sumr
Fri, 18 Feb 2005 11:48:42 +0100 nipkow tuning
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip