src/HOL/SetInterval.thy
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
2005-05-02 nipkow 2005-05-02 turned 2 lemmas into simp rules
2005-03-02 nipkow 2005-03-02 another reorganization of setsums and intervals
2005-03-01 nipkow 2005-03-01 integrated Jeremy's FiniteLib
2005-02-21 nipkow 2005-02-21 more fine tuniung
2005-02-21 nipkow 2005-02-21 comprehensive cleanup, replacing sumr by setsum
2004-12-17 paulson 2004-12-17 removed two looping simplifications in SetInterval.thy; deleted the .ML file
2004-12-12 nipkow 2004-12-12 REorganized Finite_Set
2004-10-19 paulson 2004-10-19 converted some induct_tac to induct
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-07-16 nipkow 2004-07-16 Fine-tuned sum syntax.
2004-07-16 nipkow 2004-07-16 Added nice latex syntax.
2004-07-15 nipkow 2004-07-15 more syntax
2004-07-15 paulson 2004-07-15 redefining sumr to be a translation to setsum
2004-07-15 nipkow 2004-07-15 Moved to new m<..<n syntax for set intervals.
2004-07-14 nipkow 2004-07-14 added {0::nat..n(} = {..n(}
2004-07-13 nipkow 2004-07-13 Got rid of Summation and made it a translation into setsum instead.
2004-05-29 wenzelm 2004-05-29 \<^bsub>/\<^esub> syntax: unbreakable block;
2004-05-01 wenzelm 2004-05-01 improved subscript syntax;
2004-04-16 wenzelm 2004-04-16 tuned document;
2004-03-25 paulson 2004-03-25 new material from Avigad
2004-03-19 nipkow 2004-03-19 added a few 0 and Suc lemmas
2004-03-01 kleing 2004-03-01 union/intersection over intervals
2004-02-19 ballarin 2004-02-19 Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier.
2003-03-06 paulson 2003-03-06 new logical equivalences
2002-11-28 ballarin 2002-11-28 HOL-Algebra partially ported to Isar.
2001-09-27 wenzelm 2001-09-27 eliminated theories "equalities" and "mono" (made part of "Typedef", which supercedes "subset");
2000-10-13 nipkow 2000-10-13 *** empty log message ***
2000-10-12 nipkow 2000-10-12 *** empty log message ***
2000-05-24 paulson 2000-05-24 added parent
2000-05-23 nipkow 2000-05-23 Added SetInterval