Subscripts for theorem lists now start at 1.
authorberghofe
Thu Feb 10 10:43:57 2005 +0100 (2005-02-10)
changeset 155173bc57d428ec1
parent 15516 a4bbed7487ea
child 15518 81e5f6d3ab1d
Subscripts for theorem lists now start at 1.
src/HOL/Finite_Set.thy
src/Pure/pure_thy.ML
     1.1 --- a/src/HOL/Finite_Set.thy	Thu Feb 10 08:25:22 2005 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Thu Feb 10 10:43:57 2005 +0100
     1.3 @@ -1973,7 +1973,7 @@
     1.4    case singleton thus ?case by simp
     1.5  next
     1.6    case (insert x F)
     1.7 -  from insert(4) have "a = x \<or> a \<in> F" by simp
     1.8 +  from insert(5) have "a = x \<or> a \<in> F" by simp
     1.9    thus ?case
    1.10    proof
    1.11      assume "a = x" thus ?thesis using insert by(simp add:below_def ACI)
    1.12 @@ -2083,7 +2083,7 @@
    1.13  next
    1.14    case (insert y A)
    1.15    have fin: "finite {x \<squnion> a |a. a \<in> A}"
    1.16 -    by(fast intro: finite_surj[where f = "%a. x \<squnion> a", OF insert(0)])
    1.17 +    by(fast intro: finite_surj[where f = "%a. x \<squnion> a", OF insert(1)])
    1.18    have "x \<squnion> \<Sqinter> (insert y A) = x \<squnion> (y \<sqinter> \<Sqinter> A)"
    1.19      using insert by(simp add:ACf.fold1_insert_def[OF ACf_inf Inf_def])
    1.20    also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> \<Sqinter> A)" by(rule sup_inf_distrib1)
    1.21 @@ -2105,12 +2105,12 @@
    1.22  next
    1.23    case (insert x A)
    1.24    have finB: "finite {x \<squnion> b |b. b \<in> B}"
    1.25 -    by(fast intro: finite_surj[where f = "%b. x \<squnion> b", OF B(0)])
    1.26 +    by(fast intro: finite_surj[where f = "%b. x \<squnion> b", OF B(1)])
    1.27    have finAB: "finite {a \<squnion> b |a b. a \<in> A \<and> b \<in> B}"
    1.28    proof -
    1.29      have "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {a \<squnion> b})"
    1.30        by blast
    1.31 -    thus ?thesis by(simp add: insert(0) B(0))
    1.32 +    thus ?thesis by(simp add: insert(1) B(1))
    1.33    qed
    1.34    have ne: "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
    1.35    have "\<Sqinter>(insert x A) \<squnion> \<Sqinter>B = (x \<sqinter> \<Sqinter>A) \<squnion> \<Sqinter>B"
     2.1 --- a/src/Pure/pure_thy.ML	Thu Feb 10 08:25:22 2005 +0100
     2.2 +++ b/src/Pure/pure_thy.ML	Thu Feb 10 10:43:57 2005 +0100
     2.3 @@ -143,7 +143,7 @@
     2.4  
     2.5  fun select_thm (s, None) xs = xs
     2.6    | select_thm (s, Some is) xs = map
     2.7 -      (fn i => nth_elem (i, xs) handle LIST _ =>
     2.8 +      (fn i => if i < 1 then raise LIST "" else nth_elem (i-1, xs) handle LIST _ =>
     2.9           error ("Bad subscript " ^ string_of_int i ^ " for " ^ quote s)) is;
    2.10  
    2.11