# HG changeset patch
# User nipkow
# Date 1247654681 -7200
# Node ID c369417be0552fbebb647b51d719e1d482a4ceec
# Parent  6ef7056e5215cfc11cbf2c4c23f5a28c70aa4e26
made upt/upto executable on nat/int by simp

diff -r 6ef7056e5215 -r c369417be055 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Jul 14 12:18:52 2009 +0200
+++ b/src/HOL/List.thy	Wed Jul 15 12:44:41 2009 +0200
@@ -2268,6 +2268,8 @@
 -- {* simp does not terminate! *}
 by (induct j) auto
 
+lemmas upt_rec_number_of[simp] = upt_rec[of "number_of m" "number_of n", standard]
+
 lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
 by (subst upt_rec) simp
 
@@ -3202,6 +3204,8 @@
 lemma upto_rec2_int: "(i::int) \<le> j \<Longrightarrow> [i..j+1] = [i..j] @ [j+1]"
 by(rule upto_rec2[where 'a = int, simplified successor_int_def])
 
+lemmas upto_rec_number_of_int[simp] = upto_rec[of "number_of m :: int" "number_of n", standard]
+
 
 subsubsection {* @{text lists}: the list-forming operator over sets *}