--- a/src/HOL/List.thy Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/List.thy Sat Oct 17 14:43:18 2009 +0200
@@ -3935,15 +3935,15 @@
assume L: ?L
show ?R
proof clarify
- fix n assume n: "n : {i..<j}"
- show "P n"
- proof cases
- assume "n = i" thus "P n" using L by simp
- next
- assume "n ~= i"
- hence "i+1 <= n" using n by auto
- thus "P n" using L n by simp
- qed
+ fix n assume n: "n : {i..<j}"
+ show "P n"
+ proof cases
+ assume "n = i" thus "P n" using L by simp
+ next
+ assume "n ~= i"
+ hence "i+1 <= n" using n by auto
+ thus "P n" using L n by simp
+ qed
qed
next
assume R: ?R thus ?L using `?yes` 1 by auto
@@ -3990,15 +3990,15 @@
assume L: ?L
show ?R
proof clarify
- fix n assume n: "n : {i..j}"
- show "P n"
- proof cases
- assume "n = i" thus "P n" using L by simp
- next
- assume "n ~= i"
- hence "i+1 <= n" using n by auto
- thus "P n" using L n by simp
- qed
+ fix n assume n: "n : {i..j}"
+ show "P n"
+ proof cases
+ assume "n = i" thus "P n" using L by simp
+ next
+ assume "n ~= i"
+ hence "i+1 <= n" using n by auto
+ thus "P n" using L n by simp
+ qed
qed
next
assume R: ?R thus ?L using `?yes` 1 by auto