# HG changeset patch
# User nipkow
# Date 1220299842 -7200
# Node ID a45e8c872dc19848a29f7988b52db8340af5c64a
# Parent  6ab5b4595f6438dda646430a62d506d09c07728c
It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...

diff -r 6ab5b4595f64 -r a45e8c872dc1 src/HOL/List.thy
--- 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