2007-05-17 huffman 2007-05-17 instance division_ring < no_zero_divisors; clean up field instance proofs
2007-05-17 huffman 2007-05-17 remove redundant instance declaration
2007-05-17 huffman 2007-05-17 cleaned up proof of Maclaurin_sin_bound
2007-05-16 huffman 2007-05-16 section labels
2007-05-16 huffman 2007-05-16 minimize imports
2007-05-16 chaieb 2007-05-16 dropped |R
2007-05-15 chaieb 2007-05-15 A verified theory for rational numbers representation and simple calculations; verified with respect to the real numbers;
2007-05-15 berghofe 2007-05-15 Fixed bug that caused proof of induction theorem to fail if introduction rules contained True or False.
2007-05-15 huffman 2007-05-15 minimize imports
2007-05-15 huffman 2007-05-15 clean up polar_Ex proofs; remove unnecessary lemmas
2007-05-15 huffman 2007-05-15 remove simp attribute from various polar_Ex lemmas
2007-05-14 huffman 2007-05-14 tuned proofs
2007-05-14 huffman 2007-05-14 spelling: rename arcos -> arccos
2007-05-14 huffman 2007-05-14 tuned proofs
2007-05-14 huffman 2007-05-14 add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules
2007-05-14 huffman 2007-05-14 generalized sgn function to work on any real normed vector space
2007-05-14 huffman 2007-05-14 root and sqrt on negative inputs
2007-05-14 huffman 2007-05-14 move lemmas to RealPow.thy; tuned proofs
2007-05-14 huffman 2007-05-14 tuned proofs
2007-05-14 huffman 2007-05-14 tuned
2007-05-14 huffman 2007-05-14 added general sum-squares lemmas
2007-05-14 huffman 2007-05-14 new lemmas
2007-05-14 webertj 2007-05-14 ProofGeneral: Find Theorems search form
2007-05-14 haftmann 2007-05-14 reorganized float arithmetic
2007-05-14 haftmann 2007-05-14 fixed IntInf ambiguity
2007-05-14 huffman 2007-05-14 remove redundant lemmas
2007-05-14 huffman 2007-05-14 remove redundant lemmas
2007-05-14 huffman 2007-05-14 remove redundant lemmas
2007-05-14 huffman 2007-05-14 remove redundant lemmas
2007-05-14 huffman 2007-05-14 cleaned up
2007-05-14 huffman 2007-05-14 tuned
2007-05-13 huffman 2007-05-13 define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously
2007-05-13 huffman 2007-05-13 add lemma power_eq_imp_eq_base
2007-05-13 haftmann 2007-05-13 added module int
2007-05-13 haftmann 2007-05-13 dropped legacy
2007-05-13 haftmann 2007-05-13 removed module rat.ML
2007-05-13 haftmann 2007-05-13 whitespace tuned
2007-05-13 haftmann 2007-05-13 tuned
2007-05-13 haftmann 2007-05-13 fixed omission
2007-05-13 haftmann 2007-05-13 tuned setup
2007-05-13 haftmann 2007-05-13 refined module rat
2007-05-13 haftmann 2007-05-13 added modules rat.ML and int.ML
2007-05-13 nipkow 2007-05-13 Removed junk
2007-05-13 nipkow 2007-05-13 Got rid of listsp
2007-05-13 huffman 2007-05-13 removed redundant lemmas
2007-05-12 huffman 2007-05-12 add lemma additive.setsum
2007-05-11 nipkow 2007-05-11 *** empty log message ***
2007-05-11 nipkow 2007-05-11 *** empty log message ***
2007-05-11 wenzelm 2007-05-11 proper type for fun/arg_cong_rule;
2007-05-11 wenzelm 2007-05-11 added fun/arg_cong_rule;
2007-05-11 wenzelm 2007-05-11 unified names: foo_conv;
2007-05-11 wenzelm 2007-05-11 tuned;
2007-05-11 krauss 2007-05-11 added fun flip f x y = f y x
2007-05-11 huffman 2007-05-11 generalize setsum lemmas from semiring_0_cancel to semiring_0
2007-05-11 wenzelm 2007-05-11 tuned proofs;
2007-05-11 wenzelm 2007-05-11 bang_facts: warning;
2007-05-11 wenzelm 2007-05-11 tuned proofs;
2007-05-10 haftmann 2007-05-10 (class target)
2007-05-10 haftmann 2007-05-10 cleaned up
2007-05-10 haftmann 2007-05-10 beta/eta conversion after preprocessor