src/HOL/SetInterval.thy
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
2009-11-04 nipkow 2009-11-04 fixed order of parameters in induction rules
2009-10-29 haftmann 2009-10-29 moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
2009-10-20 paulson 2009-10-20 Some new lemmas concerning sets
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-09-17 paulson 2009-09-17 New theorems for proving equalities and inclusions involving unions
2009-08-31 nipkow 2009-08-31 tuned the simp rules for Int involving insert and intervals.
2009-08-28 nipkow 2009-08-28 Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
2009-08-26 nipkow 2009-08-26 new interval lemma CCS example for predicate compiler
2009-08-26 nipkow 2009-08-26 new lemmas
2009-07-15 nipkow 2009-07-15 More finite set induction rules
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-06-08 nipkow 2009-06-08 more lemmas
2009-06-08 nipkow 2009-06-08 new lemma
2009-06-08 nipkow 2009-06-08 New lemma
2009-06-04 nipkow 2009-06-04 A few finite lemmas
2009-05-06 nipkow 2009-05-06 new lemmas
2009-04-28 haftmann 2009-04-28 stripped class recpower further
2009-03-09 nipkow 2009-03-09 fixed typing of UN/INT syntax
2009-03-09 nipkow 2009-03-09 UN syntax fix
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-23 huffman 2009-02-23 make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
2009-02-18 paulson 2009-02-18 Syntactic support for products over set intervals
2009-02-15 nipkow 2009-02-15 more finiteness
2009-02-02 haftmann 2009-02-02 fixed proposition slip
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2008-11-19 nipkow 2008-11-19 Added new fold operator and renamed the old oe to fold_image.
2008-09-01 nipkow 2008-09-01 cleaned up code generation for {.._} and {..<_} moved lemmas into SetInterval where they belong
2008-07-19 bulwahn 2008-07-19 added verification framework for the HeapMonad and quicksort as example for this framework
2008-02-21 nipkow 2008-02-21 moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and added some
2008-02-15 haftmann 2008-02-15 <= and < on nat no longer depend on wellfounded relations
2008-01-15 haftmann 2008-01-15 joined theories IntDef, Numeral, IntArith to theory Int
2007-12-06 haftmann 2007-12-06 dropped legacy bindings
2007-10-16 haftmann 2007-10-16 global class syntax
2007-10-05 nipkow 2007-10-05 added lemmas
2007-09-29 haftmann 2007-09-29 proper syntax during class specification
2007-09-24 nipkow 2007-09-24 localized { .. } (but only a few thms)
2007-08-28 nipkow 2007-08-28 added (code) lemmas for setsum and foldl
2007-08-15 paulson 2007-08-15 ATP blacklisting is now in theory data, attribute noatp
2007-06-25 nipkow 2007-06-25 removed redundant lemmas
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
2007-06-20 huffman 2007-06-20 change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
2007-06-17 nipkow 2007-06-17 tuned laws for cancellation in divisions for fields.
2007-06-15 nipkow 2007-06-15 made divide_self a simp rule
2007-06-06 huffman 2007-06-06 generalize class constraints on some lemmas
2007-04-16 huffman 2007-04-16 generalized type of lemma geometric_sum
2006-11-23 wenzelm 2006-11-23 prefer antiquotations over LaTeX macros;
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-05-02 wenzelm 2006-05-02 actually removed old stuff;
2006-04-26 kleing 2006-04-26 moved arithmetic series to geometric series in SetInterval
2006-04-09 nipkow 2006-04-09 Removed old set interval syntax.
2006-02-19 kleing 2006-02-19 * added Library/ASeries (sum of arithmetic series with instantiation to nat and int) * added Complex/ex/ASeries_Complex (instantiation of the above for reals) * added Complex/ex/HarmonicSeries (should really be in something like Complex/Library) (these are contributions by Benjamin Porter, numbers 68 and 34 of http://www.cs.ru.nl/~freek/100/)
2006-02-12 kleing 2006-02-12 * moved ThreeDivides from Isar_examples to better suited HOL/ex * moved 2 summation lemmas from ThreeDivides to SetInterval
2005-09-29 nipkow 2005-09-29 Added a few lemmas
2005-08-26 ballarin 2005-08-26 Lemmas on dvd, power and finite summation added or strengthened.
2005-07-07 nipkow 2005-07-07 linear arithmetic now takes "&" in assumptions apart.
2005-05-27 ballarin 2005-05-27 Locale expressions: rename with optional mixfix syntax.
2005-05-23 nipkow 2005-05-23 tuned setsum rewrites
2005-05-23 nipkow 2005-05-23 simplifier trace info; Suc-intervals