author berghofe Thu Feb 10 10:43:57 2005 +0100 (2005-02-10) changeset 15517 3bc57d428ec1 parent 15516 a4bbed7487ea child 15518 81e5f6d3ab1d
Subscripts for theorem lists now start at 1.
 src/HOL/Finite_Set.thy file | annotate | diff | revisions src/Pure/pure_thy.ML file | annotate | diff | revisions
```     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
```