changeset 28072 | a45e8c872dc1 |
parent 28068 | f6b2d1995171 |
child 28090 | 29af3c712d2b |
--- a/src/HOL/List.thy Mon Sep 01 19:17:47 2008 +0200 +++ b/src/HOL/List.thy Mon Sep 01 22:10:42 2008 +0200 @@ -3626,6 +3626,14 @@ text {* Code for bounded quantification and summation over nats. *} +lemma atMost_upto [code unfold]: + "{..n} = set [0..<Suc n]" +by auto + +lemma atLeast_upt [code unfold]: + "{..<n} = set [0..<n]" +by auto + lemma greaterThanLessThan_upt [code unfold]: "{n<..<m} = set [Suc n..<m]" by auto