2007-06-10 wenzelm 2007-06-10 disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
2007-06-10 nipkow 2007-06-10 *** empty log message ***
2007-06-09 huffman 2007-06-09 remove dependencies of proofs on constant int::nat=>int, preparing to remove it
2007-06-09 wenzelm 2007-06-09 eqtype int -- explicitly encourage overloaded equality; tuned -%; removed obsolete Intt;
2007-06-09 wenzelm 2007-06-09 simplified type integer;
2007-06-08 berghofe 2007-06-08 Adapted Proofterm.bicompose_proof to Larry's changes in Logic.assum_pairs from 2005-01-24 (revision 1.44).
2007-06-08 chaieb 2007-06-08 Method "algebra" solves polynomial equations over (semi)rings
2007-06-08 huffman 2007-06-08 generalize zpower_number_of_{even,odd} lemmas
2007-06-07 obua 2007-06-07 deleted comments
2007-06-07 obua 2007-06-07 deleted legacy lemmas
2007-06-07 nipkow 2007-06-07 somebody elses problem fixed
2007-06-07 nipkow 2007-06-07 filter syntax change
2007-06-07 huffman 2007-06-07 remove redundant lemmas
2007-06-07 huffman 2007-06-07 remove references to preal-specific theorems
2007-06-07 huffman 2007-06-07 define (1::preal); clean up instance declarations
2007-06-07 huffman 2007-06-07 tuned
2007-06-07 huffman 2007-06-07 instance preal :: ordered_cancel_ab_semigroup_add
2007-06-06 huffman 2007-06-06 use new-style class for sq_ord; rename op << to sq_le
2007-06-06 urbanc 2007-06-06 take out Class.thy again, because it does not yet compile cleanly
2007-06-06 huffman 2007-06-06 add axclass semiring_char_0 for types where of_nat is injective
2007-06-06 nipkow 2007-06-06 changed filter syntax from : to <-
2007-06-06 nipkow 2007-06-06 hide filter
2007-06-06 nipkow 2007-06-06 tuned list comprehension, changed filter syntax from : to <-
2007-06-06 huffman 2007-06-06 clean up proofs of exp_zero, sin_zero, cos_zero
2007-06-06 huffman 2007-06-06 generalize class constraints on some lemmas
2007-06-06 huffman 2007-06-06 generalize of_nat and related constants to class semiring_1
2007-06-06 huffman 2007-06-06 declare complex_diff as simp rule
2007-06-06 chaieb 2007-06-06 New Reflected Presburger added to HOL/ex
2007-06-05 wenzelm 2007-06-05 Groebner Basis Examples.
2007-06-05 wenzelm 2007-06-05 print_antiquotations: sort_strings;
2007-06-05 wenzelm 2007-06-05 tuned document; added Groebner_Examples;
2007-06-05 wenzelm 2007-06-05 tuned source deps;
2007-06-05 wenzelm 2007-06-05 simplified/renamed add_numerals;
2007-06-05 wenzelm 2007-06-05 renamed ex/Eval_Examples.thy;
2007-06-05 wenzelm 2007-06-05 added ex/Groebner_Examples.thy; renamed ex/Eval_Examples.thy;
2007-06-05 wenzelm 2007-06-05 tuned document;
2007-06-05 chaieb 2007-06-05 Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic
2007-06-05 chaieb 2007-06-05 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
2007-06-05 haftmann 2007-06-05 tuned boostrap
2007-06-05 haftmann 2007-06-05 eliminated Code_Generator.thy
2007-06-05 haftmann 2007-06-05 tuned integers
2007-06-05 wenzelm 2007-06-05 tuned;
2007-06-05 wenzelm 2007-06-05 fixed type int vs. integer;
2007-06-05 wenzelm 2007-06-05 renamed locale ring/semiring to gb_ring/gb_semiring to avoid clash with Ring_and_Field versions;
2007-06-05 huffman 2007-06-05 add new lemmas
2007-06-05 chaieb 2007-06-05 Polynomials now only depend on Deriv; Definition of degree changed
2007-06-05 chaieb 2007-06-05 lemma lemma_DERIV_subst moved to Deriv.thy
2007-06-05 wenzelm 2007-06-05 tuned proofs;
2007-06-05 wenzelm 2007-06-05 tuned comments;
2007-06-05 wenzelm 2007-06-05 Semiring normalization and Groebner Bases.
2007-06-05 haftmann 2007-06-05 moved generic algebra modules
2007-06-05 haftmann 2007-06-05 updated documentation
2007-06-05 haftmann 2007-06-05 fixed broken execption handling
2007-06-05 haftmann 2007-06-05 simplified notion of "operational classes"
2007-06-05 haftmann 2007-06-05 merged Code_Generator.thy into HOL.thy
2007-06-05 chaieb 2007-06-05 added a function partition and a few lemmas
2007-06-05 chaieb 2007-06-05 added a few theorems about foldl and set
2007-06-05 chaieb 2007-06-05 added lcm, ilcm (lcm for integers) and some lemmas about them;
2007-06-05 urbanc 2007-06-05 included Class.thy in the compiling process for Nominal/Examples
2007-06-05 huffman 2007-06-05 remove simp attribute from lemma_STAR theorems