diff -r d0e3f790bd73 -r 15f7a6745cce doc-src/TutorialI/Inductive/AB.thy
--- a/doc-src/TutorialI/Inductive/AB.thy	Thu Jun 14 00:48:42 2007 +0200
+++ b/doc-src/TutorialI/Inductive/AB.thy	Thu Jun 14 07:27:55 2007 +0200
@@ -68,13 +68,13 @@
 *}
 
 lemma correctness:
-  "(w \<in> S \<longrightarrow> size[x\<in>w. x=a] = size[x\<in>w. x=b])     \<and>
-   (w \<in> A \<longrightarrow> size[x\<in>w. x=a] = size[x\<in>w. x=b] + 1) \<and>
-   (w \<in> B \<longrightarrow> size[x\<in>w. x=b] = size[x\<in>w. x=a] + 1)"
+  "(w \<in> S \<longrightarrow> size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b])     \<and>
+   (w \<in> A \<longrightarrow> size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b] + 1) \<and>
+   (w \<in> B \<longrightarrow> size[x\<leftarrow>w. x=b] = size[x\<leftarrow>w. x=a] + 1)"
 
 txt{*\noindent
 These propositions are expressed with the help of the predefined @{term
-filter} function on lists, which has the convenient syntax @{text"[x\<in>xs. P
+filter} function on lists, which has the convenient syntax @{text"[x\<leftarrow>xs. P
 x]"}, the list of all elements @{term x} in @{term xs} such that @{prop"P x"}
 holds. Remember that on lists @{text size} and @{text length} are synonymous.
 
@@ -116,8 +116,8 @@
 *}
 
 lemma step1: "\<forall>i < size w.
-  \<bar>(int(size[x\<in>take (i+1) w. P x])-int(size[x\<in>take (i+1) w. \<not>P x]))
-   - (int(size[x\<in>take i w. P x])-int(size[x\<in>take i w. \<not>P x]))\<bar> \<le> 1"
+  \<bar>(int(size[x\<leftarrow>take (i+1) w. P x])-int(size[x\<leftarrow>take (i+1) w. \<not>P x]))
+   - (int(size[x\<leftarrow>take i w. P x])-int(size[x\<leftarrow>take i w. \<not>P x]))\<bar> \<le> 1"
 
 txt{*\noindent
 The lemma is a bit hard to read because of the coercion function
@@ -141,8 +141,8 @@
 *}
 
 lemma part1:
- "size[x\<in>w. P x] = size[x\<in>w. \<not>P x]+2 \<Longrightarrow>
-  \<exists>i\<le>size w. size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>P x]+1"
+ "size[x\<leftarrow>w. P x] = size[x\<leftarrow>w. \<not>P x]+2 \<Longrightarrow>
+  \<exists>i\<le>size w. size[x\<leftarrow>take i w. P x] = size[x\<leftarrow>take i w. \<not>P x]+1"
 
 txt{*\noindent
 This is proved by @{text force} with the help of the intermediate value theorem,
@@ -161,10 +161,10 @@
 
 
 lemma part2:
-  "\<lbrakk>size[x\<in>take i w @ drop i w. P x] =
-    size[x\<in>take i w @ drop i w. \<not>P x]+2;
-    size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>P x]+1\<rbrakk>
-   \<Longrightarrow> size[x\<in>drop i w. P x] = size[x\<in>drop i w. \<not>P x]+1"
+  "\<lbrakk>size[x\<leftarrow>take i w @ drop i w. P x] =
+    size[x\<leftarrow>take i w @ drop i w. \<not>P x]+2;
+    size[x\<leftarrow>take i w. P x] = size[x\<leftarrow>take i w. \<not>P x]+1\<rbrakk>
+   \<Longrightarrow> size[x\<leftarrow>drop i w. P x] = size[x\<leftarrow>drop i w. \<not>P x]+1"
 by(simp del: append_take_drop_id)
 
 text{*\noindent
@@ -191,9 +191,9 @@
 *}
 
 theorem completeness:
-  "(size[x\<in>w. x=a] = size[x\<in>w. x=b]     \<longrightarrow> w \<in> S) \<and>
-   (size[x\<in>w. x=a] = size[x\<in>w. x=b] + 1 \<longrightarrow> w \<in> A) \<and>
-   (size[x\<in>w. x=b] = size[x\<in>w. x=a] + 1 \<longrightarrow> w \<in> B)"
+  "(size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b]     \<longrightarrow> w \<in> S) \<and>
+   (size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b] + 1 \<longrightarrow> w \<in> A) \<and>
+   (size[x\<leftarrow>w. x=b] = size[x\<leftarrow>w. x=a] + 1 \<longrightarrow> w \<in> B)"
 
 txt{*\noindent
 The proof is by induction on @{term w}. Structural induction would fail here
@@ -237,9 +237,9 @@
  apply(clarify)
 txt{*\noindent
 This yields an index @{prop"i \<le> length v"} such that
-@{prop[display]"length [x\<in>take i v . x = a] = length [x\<in>take i v . x = b] + 1"}
+@{prop[display]"length [x\<leftarrow>take i v . x = a] = length [x\<leftarrow>take i v . x = b] + 1"}
 With the help of @{thm[source]part2} it follows that
-@{prop[display]"length [x\<in>drop i v . x = a] = length [x\<in>drop i v . x = b] + 1"}
+@{prop[display]"length [x\<leftarrow>drop i v . x = a] = length [x\<leftarrow>drop i v . x = b] + 1"}
 *}
 
  apply(drule part2[of "\<lambda>x. x=a", simplified])