# HG changeset patch
# User berghofe
# Date 1108028637 -3600
# Node ID 3bc57d428ec1dd3b9ab088f7ccc7c5afbf246f61
# Parent  a4bbed7487ea695ad6133c882b4f2ce08a9396dd
Subscripts for theorem lists now start at 1.

diff -r a4bbed7487ea -r 3bc57d428ec1 src/HOL/Finite_Set.thy
--- 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"
diff -r a4bbed7487ea -r 3bc57d428ec1 src/Pure/pure_thy.ML
--- 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;