2009-02-23 huffman 2009-02-23 explicitly import Fact
2009-02-23 huffman 2009-02-23 change imports to move Fact.thy outside Plain
2009-02-23 huffman 2009-02-23 add lemmas poly_{div,mod}_minus_{left,right}
2009-02-23 huffman 2009-02-23 merged
2009-02-22 huffman 2009-02-22 declare scaleR distrib rules [algebra_simps]; cleaned up
2009-02-22 huffman 2009-02-22 clean up instantiations
2009-02-22 huffman 2009-02-22 merged
2009-02-22 huffman 2009-02-22 simplify some proofs
2009-02-22 huffman 2009-02-22 remove duplicate instance declaration
2009-02-23 haftmann 2009-02-23 stripped classrels_of, instances_of
2009-02-23 haftmann 2009-02-23 use canonical subalgebra projection
2009-02-22 haftmann 2009-02-22 experimental switch to new well-sorting algorithm
2009-02-22 haftmann 2009-02-22 handle NONE case in arity function properly
2009-02-22 haftmann 2009-02-22 clarified status of variables in evaluation terms; tuned header
2009-02-22 haftmann 2009-02-22 subalgebra: drop arities if desired
2009-02-22 haftmann 2009-02-22 merged
2009-02-22 haftmann 2009-02-22 more liberality needed
2009-02-22 nipkow 2009-02-22 merged
2009-02-22 nipkow 2009-02-22 added lemmas
2009-02-22 haftmann 2009-02-22 merged
2009-02-22 haftmann 2009-02-22 simplified evaluation
2009-02-22 nipkow 2009-02-22 merged
2009-02-22 nipkow 2009-02-22 added dvd_div_mult
2009-02-22 haftmann 2009-02-22 merged
2009-02-22 haftmann 2009-02-22 first attempt to solve evaluation bootstrap problem
2009-02-22 haftmann 2009-02-22 formal dependency on newly emerging algorithm
2009-02-22 nipkow 2009-02-22 merged
2009-02-22 nipkow 2009-02-22 name fix
2009-02-21 huffman 2009-02-21 fix spelling
2009-02-21 huffman 2009-02-21 real_inner class instance for vectors
2009-02-21 nipkow 2009-02-21 NEWS
2009-02-21 nipkow 2009-02-21 merged
2009-02-21 nipkow 2009-02-21 Removed subsumed lemmas
2009-02-21 huffman 2009-02-21 remove duplicated lemmas about norm
2009-02-21 huffman 2009-02-21 real_normed_vector instance
2009-02-21 huffman 2009-02-21 fix real_vector, real_algebra instances
2009-02-21 huffman 2009-02-21 merged
2009-02-20 huffman 2009-02-20 generalize lemmas from nat to 'a::wellorder
2009-02-20 huffman 2009-02-20 generalize some lemmas
2009-02-21 nipkow 2009-02-21 merged
2009-02-21 nipkow 2009-02-21 removed redundant thms
2009-02-20 huffman 2009-02-20 merged
2009-02-20 huffman 2009-02-20 class instances for num1
2009-02-20 nipkow 2009-02-20 Removed redundant lemmas
2009-02-20 haftmann 2009-02-20 merged
2009-02-20 haftmann 2009-02-20 also consider superclasses properly
2009-02-20 nipkow 2009-02-20 merged
2009-02-20 nipkow 2009-02-20 removed subsumed lemmas
2009-02-20 haftmann 2009-02-20 merged
2009-02-20 haftmann 2009-02-20 datatype antiquotation: always bracket types with spaces in between
2009-02-20 haftmann 2009-02-20 consequent use of term `code equation`
2009-02-20 haftmann 2009-02-20 permissive check for pattern discipline in case schemes
2009-02-20 haftmann 2009-02-20 maintain order of constructors in datatypes; clarified conventions for type schemes
2009-02-20 haftmann 2009-02-20 stripped Id
2009-02-20 huffman 2009-02-20 merged
2009-02-20 huffman 2009-02-20 add theory of products as real vector spaces to Library
2009-02-20 huffman 2009-02-20 add new theory Product_plus.thy to Library
2009-02-20 immler 2009-02-20 merged
2009-02-20 immler 2009-02-20 changed message
2009-02-20 immler 2009-02-20 detailed information on atp-failure via Output.debug