2005-03-08 obua 2005-03-08 fix integer overflow in numeral syntax for SML NJ.
2005-03-08 huffman 2005-03-08 fixed variable name
2005-03-08 huffman 2005-03-08 reordered and arranged for document generation, cleaned up some proofs
2005-03-08 huffman 2005-03-08 removed Cprod3_lemma1 and Cprod3_lemma2
2005-03-08 huffman 2005-03-08 reordered and arranged for document generation, cleaned up some proofs
2005-03-08 huffman 2005-03-08 added subsection headings, cleaned up some proofs
2005-03-08 huffman 2005-03-08 reordered and arranged for document generation, cleaned up some proofs
2005-03-08 huffman 2005-03-08 arranged for document generation, cleaned up some proofs
2005-03-07 huffman 2005-03-07 added subsections and text for document generation
2005-03-07 huffman 2005-03-07 Added dependency document/root.tex, and -g true option to isatool; document generation should work now.
2005-03-07 webertj 2005-03-07 HTML 4.01 Transitional conformity
2005-03-07 webertj 2005-03-07 refute_params: default value itself=1 added (for type classes)
2005-03-07 webertj 2005-03-07 HTML 4.01 Transitional conformity
2005-03-07 webertj 2005-03-07 HTML 4.01 Transitional conformity
2005-03-07 paulson 2005-03-07 now checks for higher-order vars
2005-03-07 obua 2005-03-07 Cleaning up HOL/Matrix
2005-03-07 paulson 2005-03-07 Tools/meson.ML: signature, structure and "open" rather than "local"
2005-03-04 huffman 2005-03-04 add header
2005-03-04 huffman 2005-03-04 fix headers
2005-03-04 huffman 2005-03-04 converted to new-style theories, and combined numbered files
2005-03-04 huffman 2005-03-04 document generation for HOLCF
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-04 paulson 2005-03-04 new first_order test
2005-03-04 paulson 2005-03-04 removed dead code
2005-03-03 webertj 2005-03-03 interpreter for Finite_Set.Finites added
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-03-03 nipkow 2005-03-03 fixed proof
2005-03-03 huffman 2005-03-03 converted to new-style theory
2005-03-03 huffman 2005-03-03 converted to new-style theory
2005-03-02 huffman 2005-03-02 converted to new-style theory
2005-03-02 huffman 2005-03-02 converted to new-style theory
2005-03-02 huffman 2005-03-02 converted to new-style theory
2005-03-02 huffman 2005-03-02 converted to new-style theory
2005-03-02 huffman 2005-03-02 converted to new-style theory
2005-03-02 nipkow 2005-03-02 another reorganization of setsums and intervals
2005-03-02 dixon 2005-03-02 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.
2005-03-02 paulson 2005-03-02 obscured the e-mail address lcp@cl
2005-03-02 paulson 2005-03-02 new lemmas int_diff_cases
2005-03-02 huffman 2005-03-02 eliminated deps for removed files
2005-03-02 huffman 2005-03-02 merged into Discrete.thy
2005-03-02 huffman 2005-03-02 converted to new-style theory
2005-03-01 nipkow 2005-03-01 integrated Jeremy's FiniteLib
2005-03-01 kleing 2005-03-01 spider dogding
2005-02-28 obua 2005-02-28 added setsum_diff1' which holds in more general cases than setsum_diff1
2005-02-28 paulson 2005-02-28 unfold theorems for trancl and rtrancl
2005-02-27 dixon 2005-02-27 lucas - added more comments and an extra type to clarify the code.
2005-02-23 berghofe 2005-02-23 Modified node_trans to avoid duplication of signature stamps when undoing.
2005-02-23 webertj 2005-02-23 exception SAME removed
2005-02-23 webertj 2005-02-23 major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
2005-02-23 nipkow 2005-02-23 suminf -> \<Sum>
2005-02-22 dixon 2005-02-22 Lucas - fixed bug in zero_var_indexes: it was ignoring vars in the flex-flex pairs. These are now taken into account.
2005-02-22 paulson 2005-02-22 removed redundant lemmas and simprules
2005-02-22 nipkow 2005-02-22 more setsum tuning
2005-02-21 nipkow 2005-02-21 more fine tuniung
2005-02-21 nipkow 2005-02-21 fixed proof
2005-02-21 nipkow 2005-02-21 removed superfluous setsum_constant
2005-02-21 nipkow 2005-02-21 comprehensive cleanup, replacing sumr by setsum
2005-02-19 dixon 2005-02-19 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.
2005-02-18 nipkow 2005-02-18 continued eliminating sumr
2005-02-18 nipkow 2005-02-18 starting to get rid of sumr