src/HOL/SetInterval.thy
2010-11-23 hoelzl 2010-11-23 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-09-02 hoelzl 2010-09-02 Add lessThan_Suc_eq_insert_0
2010-07-01 hoelzl 2010-07-01 Instantiate product type as euclidean space.
2010-06-08 haftmann 2010-06-08 tuned quotes, antiquotations and whitespace
2010-05-11 hoelzl 2010-05-11 Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
2010-05-08 nipkow 2010-05-08 added lemmas
2010-04-26 huffman 2010-04-26 merged
2010-04-26 huffman 2010-04-26 fix syntax precedence declarations for UNION, INTER, SUP, INF
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps
2010-04-23 haftmann 2010-04-23 sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-08 haftmann 2010-03-08 transfer: avoid camel case
2010-03-04 hoelzl 2010-03-04 Rewrite rules for images of minus of intervals
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
2010-02-17 hoelzl 2010-02-17 Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
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