Subscripts for theorem lists now start at 1.
--- a/src/HOL/Finite_Set.thy Thu Feb 10 08:25:22 2005 +0100
+++ b/src/HOL/Finite_Set.thy Thu Feb 10 10:43:57 2005 +0100
@@ -1973,7 +1973,7 @@
case singleton thus ?case by simp
next
case (insert x F)
- from insert(4) have "a = x \<or> a \<in> F" by simp
+ from insert(5) have "a = x \<or> a \<in> F" by simp
thus ?case
proof
assume "a = x" thus ?thesis using insert by(simp add:below_def ACI)
@@ -2083,7 +2083,7 @@
next
case (insert y A)
have fin: "finite {x \<squnion> a |a. a \<in> A}"
- by(fast intro: finite_surj[where f = "%a. x \<squnion> a", OF insert(0)])
+ by(fast intro: finite_surj[where f = "%a. x \<squnion> a", OF insert(1)])
have "x \<squnion> \<Sqinter> (insert y A) = x \<squnion> (y \<sqinter> \<Sqinter> A)"
using insert by(simp add:ACf.fold1_insert_def[OF ACf_inf Inf_def])
also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> \<Sqinter> A)" by(rule sup_inf_distrib1)
@@ -2105,12 +2105,12 @@
next
case (insert x A)
have finB: "finite {x \<squnion> b |b. b \<in> B}"
- by(fast intro: finite_surj[where f = "%b. x \<squnion> b", OF B(0)])
+ by(fast intro: finite_surj[where f = "%b. x \<squnion> b", OF B(1)])
have finAB: "finite {a \<squnion> b |a b. a \<in> A \<and> b \<in> B}"
proof -
have "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {a \<squnion> b})"
by blast
- thus ?thesis by(simp add: insert(0) B(0))
+ thus ?thesis by(simp add: insert(1) B(1))
qed
have ne: "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
have "\<Sqinter>(insert x A) \<squnion> \<Sqinter>B = (x \<sqinter> \<Sqinter>A) \<squnion> \<Sqinter>B"
--- a/src/Pure/pure_thy.ML Thu Feb 10 08:25:22 2005 +0100
+++ b/src/Pure/pure_thy.ML Thu Feb 10 10:43:57 2005 +0100
@@ -143,7 +143,7 @@
fun select_thm (s, None) xs = xs
| select_thm (s, Some is) xs = map
- (fn i => nth_elem (i, xs) handle LIST _ =>
+ (fn i => if i < 1 then raise LIST "" else nth_elem (i-1, xs) handle LIST _ =>
error ("Bad subscript " ^ string_of_int i ^ " for " ^ quote s)) is;