equal
deleted
inserted
replaced
445 by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) |
445 by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) |
446 |
446 |
447 |
447 |
448 subsection {*Lemmas useful with the summation operator setsum*} |
448 subsection {*Lemmas useful with the summation operator setsum*} |
449 |
449 |
450 text {* For examples, see Algebra/poly/UnivPoly.thy *} |
450 text {* For examples, see Algebra/poly/UnivPoly2.thy *} |
451 |
451 |
452 subsubsection {* Disjoint Unions *} |
452 subsubsection {* Disjoint Unions *} |
453 |
453 |
454 text {* Singletons and open intervals *} |
454 text {* Singletons and open intervals *} |
455 |
455 |