# HG changeset patch
# User wenzelm
# Date 1392936400 -3600
# Node ID abc140f21caab683e6adb8e06fb3015cbbb21a41
# Parent  e4e8cbd9d780183be74c8008288bd8a52283e653
tuned proofs;
more symbols;

diff -r e4e8cbd9d780 -r abc140f21caa src/HOL/Isar_Examples/Basic_Logic.thy
--- a/src/HOL/Isar_Examples/Basic_Logic.thy	Thu Feb 20 23:16:33 2014 +0100
+++ b/src/HOL/Isar_Examples/Basic_Logic.thy	Thu Feb 20 23:46:40 2014 +0100
@@ -18,33 +18,33 @@
   @{text K}, and @{text S}.  The following (rather explicit) proofs
   should require little extra explanations. *}
 
-lemma I: "A --> A"
+lemma I: "A \<longrightarrow> A"
 proof
   assume A
   show A by fact
 qed
 
-lemma K: "A --> B --> A"
+lemma K: "A \<longrightarrow> B \<longrightarrow> A"
 proof
   assume A
-  show "B --> A"
+  show "B \<longrightarrow> A"
   proof
     show A by fact
   qed
 qed
 
-lemma S: "(A --> B --> C) --> (A --> B) --> A --> C"
+lemma S: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> A \<longrightarrow> C"
 proof
-  assume "A --> B --> C"
-  show "(A --> B) --> A --> C"
+  assume "A \<longrightarrow> B \<longrightarrow> C"
+  show "(A \<longrightarrow> B) \<longrightarrow> A \<longrightarrow> C"
   proof
-    assume "A --> B"
-    show "A --> C"
+    assume "A \<longrightarrow> B"
+    show "A \<longrightarrow> C"
     proof
       assume A
       show C
       proof (rule mp)
-        show "B --> C" by (rule mp) fact+
+        show "B \<longrightarrow> C" by (rule mp) fact+
         show B by (rule mp) fact+
       qed
     qed
@@ -60,7 +60,7 @@
   First of all, proof by assumption may be abbreviated as a single
   dot. *}
 
-lemma "A --> A"
+lemma "A \<longrightarrow> A"
 proof
   assume A
   show A by fact+
@@ -72,7 +72,7 @@
   higher-order unification.}.  Thus we may skip the rather vacuous
   body of the above proof as well. *}
 
-lemma "A --> A"
+lemma "A \<longrightarrow> A"
 proof
 qed
 
@@ -82,12 +82,12 @@
   statements involved.  The \isacommand{by} command abbreviates any
   proof with empty body, so the proof may be further pruned. *}
 
-lemma "A --> A"
+lemma "A \<longrightarrow> A"
   by rule
 
 text {* Proof by a single rule may be abbreviated as double-dot. *}
 
-lemma "A --> A" ..
+lemma "A \<longrightarrow> A" ..
 
 text {* Thus we have arrived at an adequate representation of the
   proof of a tautology that holds by a single standard
@@ -103,7 +103,7 @@
   conclusion.\footnote{The dual method is @{text elim}, acting on a
   goal's premises.} *}
 
-lemma "A --> B --> A"
+lemma "A \<longrightarrow> B \<longrightarrow> A"
 proof (intro impI)
   assume A
   show A by fact
@@ -111,7 +111,7 @@
 
 text {* Again, the body may be collapsed. *}
 
-lemma "A --> B --> A"
+lemma "A \<longrightarrow> B \<longrightarrow> A"
   by (intro impI)
 
 text {* Just like @{text rule}, the @{text intro} and @{text elim}
@@ -140,10 +140,10 @@
 
   The first version is purely backward. *}
 
-lemma "A & B --> B & A"
+lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof
-  assume "A & B"
-  show "B & A"
+  assume "A \<and> B"
+  show "B \<and> A"
   proof
     show B by (rule conjunct2) fact
     show A by (rule conjunct1) fact
@@ -158,13 +158,13 @@
   \isacommand{from} already does forward-chaining, involving the
   @{text conjE} rule here. *}
 
-lemma "A & B --> B & A"
+lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof
-  assume "A & B"
-  show "B & A"
+  assume "A \<and> B"
+  show "B \<and> A"
   proof
-    from `A & B` show B ..
-    from `A & B` show A ..
+    from `A \<and> B` show B ..
+    from `A \<and> B` show A ..
   qed
 qed
 
@@ -176,10 +176,10 @@
   that of the @{text conjE} rule, including the repeated goal
   proposition that is abbreviated as @{text ?thesis} below. *}
 
-lemma "A & B --> B & A"
+lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof
-  assume "A & B"
-  then show "B & A"
+  assume "A \<and> B"
+  then show "B \<and> A"
   proof                    -- {* rule @{text conjE} of @{text "A \<and> B"} *}
     assume B A
     then show ?thesis ..   -- {* rule @{text conjI} of @{text "B \<and> A"} *}
@@ -190,25 +190,25 @@
   body by doing forward reasoning all the time.  Only the outermost
   decomposition step is left as backward. *}
 
-lemma "A & B --> B & A"
+lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof
-  assume "A & B"
-  from `A & B` have A ..
-  from `A & B` have B ..
-  from `B` `A` show "B & A" ..
+  assume "A \<and> B"
+  from `A \<and> B` have A ..
+  from `A \<and> B` have B ..
+  from `B` `A` show "B \<and> A" ..
 qed
 
 text {* We can still push forward-reasoning a bit further, even at the
   risk of getting ridiculous.  Note that we force the initial proof
   step to do nothing here, by referring to the ``-'' proof method. *}
 
-lemma "A & B --> B & A"
+lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof -
   {
-    assume "A & B"
-    from `A & B` have A ..
-    from `A & B` have B ..
-    from `B` `A` have "B & A" ..
+    assume "A \<and> B"
+    from `A \<and> B` have A ..
+    from `A \<and> B` have B ..
+    from `B` `A` have "B \<and> A" ..
   }
   then show ?thesis ..         -- {* rule @{text impI} *}
 qed
@@ -232,10 +232,10 @@
   probably the middle one, with conjunction introduction done after
   elimination. *}
 
-lemma "A & B --> B & A"
+lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof
-  assume "A & B"
-  then show "B & A"
+  assume "A \<and> B"
+  then show "B \<and> A"
   proof
     assume B A
     then show ?thesis ..
@@ -256,9 +256,9 @@
   below involves forward-chaining from @{text "P \<or> P"}, followed by an
   explicit case-analysis on the two \emph{identical} cases. *}
 
-lemma "P | P --> P"
+lemma "P \<or> P \<longrightarrow> P"
 proof
-  assume "P | P"
+  assume "P \<or> P"
   then show P
   proof                    -- {*
     rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
@@ -291,9 +291,9 @@
   cases actually coincide.  Consequently the proof may be rephrased as
   follows. *}
 
-lemma "P | P --> P"
+lemma "P \<or> P --> P"
 proof
-  assume "P | P"
+  assume "P \<or> P"
   then show P
   proof
     assume P
@@ -307,9 +307,9 @@
   are implicitly performed when concluding the single rule step of the
   double-dot proof as follows. *}
 
-lemma "P | P --> P"
+lemma "P \<or> P --> P"
 proof
-  assume "P | P"
+  assume "P \<or> P"
   then show P ..
 qed
 
@@ -328,10 +328,10 @@
   ``arbitrary, but fixed'' element; the \isacommand{is} annotation
   binds term abbreviations by higher-order pattern matching. *}
 
-lemma "(EX x. P (f x)) --> (EX y. P y)"
+lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
 proof
-  assume "EX x. P (f x)"
-  then show "EX y. P y"
+  assume "\<exists>x. P (f x)"
+  then show "\<exists>y. P y"
   proof (rule exE)             -- {*
     rule @{text exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
   *}
@@ -348,10 +348,10 @@
   instances (by higher-order unification).  Thus we may as well prune
   the text as follows. *}
 
-lemma "(EX x. P (f x)) --> (EX y. P y)"
+lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
 proof
-  assume "EX x. P (f x)"
-  then show "EX y. P y"
+  assume "\<exists>x. P (f x)"
+  then show "\<exists>y. P y"
   proof
     fix a
     assume "P (f a)"
@@ -364,11 +364,11 @@
   ``\isakeyword{obtain}'' provides a more handsome way to do
   generalized existence reasoning. *}
 
-lemma "(EX x. P (f x)) --> (EX y. P y)"
+lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
 proof
-  assume "EX x. P (f x)"
+  assume "\<exists>x. P (f x)"
   then obtain a where "P (f a)" ..
-  then show "EX y. P y" ..
+  then show "\<exists>y. P y" ..
 qed
 
 text {* Technically, \isakeyword{obtain} is similar to
@@ -387,10 +387,10 @@
   since Isabelle/Isar supports non-atomic goals and assumptions fully
   transparently. *}
 
-theorem conjE: "A & B ==> (A ==> B ==> C) ==> C"
+theorem conjE: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"
 proof -
-  assume "A & B"
-  assume r: "A ==> B ==> C"
+  assume "A \<and> B"
+  assume r: "A \<Longrightarrow> B \<Longrightarrow> C"
   show C
   proof (rule r)
     show A by (rule conjunct1) fact
diff -r e4e8cbd9d780 -r abc140f21caa src/HOL/Isar_Examples/Cantor.thy
--- a/src/HOL/Isar_Examples/Cantor.thy	Thu Feb 20 23:16:33 2014 +0100
+++ b/src/HOL/Isar_Examples/Cantor.thy	Thu Feb 20 23:46:40 2014 +0100
@@ -24,22 +24,24 @@
   with the type $\alpha \ap \idt{set}$ and the operator
   $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$. *}
 
-theorem "EX S. S ~: range (f :: 'a => 'a set)"
+theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
 proof
-  let ?S = "{x. x ~: f x}"
-  show "?S ~: range f"
+  let ?S = "{x. x \<notin> f x}"
+  show "?S \<notin> range f"
   proof
-    assume "?S : range f"
+    assume "?S \<in> range f"
     then obtain y where "?S = f y" ..
     then show False
     proof (rule equalityCE)
-      assume "y : f y"
-      assume "y : ?S" then have "y ~: f y" ..
+      assume "y \<in> f y"
+      assume "y \<in> ?S"
+      then have "y \<notin> f y" ..
       with `y : f y` show ?thesis by contradiction
     next
-      assume "y ~: ?S"
-      assume "y ~: f y" then have "y : ?S" ..
-      with `y ~: ?S` show ?thesis by contradiction
+      assume "y \<notin> ?S"
+      assume "y \<notin> f y"
+      then have "y \<in> ?S" ..
+      with `y \<notin> ?S` show ?thesis by contradiction
     qed
   qed
 qed
@@ -51,7 +53,7 @@
   classical prover contains rules for the relevant constructs of HOL's
   set theory.  *}
 
-theorem "EX S. S ~: range (f :: 'a => 'a set)"
+theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
   by best
 
 text {* While this establishes the same theorem internally, we do not
diff -r e4e8cbd9d780 -r abc140f21caa src/HOL/Isar_Examples/Expr_Compiler.thy
--- a/src/HOL/Isar_Examples/Expr_Compiler.thy	Thu Feb 20 23:16:33 2014 +0100
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy	Thu Feb 20 23:46:40 2014 +0100
@@ -22,7 +22,7 @@
   This is both for abstract syntax and semantics, i.e.\ we use a
   ``shallow embedding'' here. *}
 
-type_synonym 'val binop = "'val => 'val => 'val"
+type_synonym 'val binop = "'val \<Rightarrow> 'val \<Rightarrow> 'val"
 
 
 subsection {* Expressions *}
@@ -39,7 +39,7 @@
 text {* Evaluation (wrt.\ some environment of variable assignments) is
   defined by primitive recursion over the structure of expressions. *}
 
-primrec eval :: "('adr, 'val) expr => ('adr => 'val) => 'val"
+primrec eval :: "('adr, 'val) expr \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val"
 where
   "eval (Variable x) env = env x"
 | "eval (Constant c) env = c"
@@ -59,17 +59,17 @@
 text {* Execution of a list of stack machine instructions is easily
   defined as follows. *}
 
-primrec exec :: "(('adr, 'val) instr) list => 'val list => ('adr => 'val) => 'val list"
+primrec exec :: "(('adr, 'val) instr) list \<Rightarrow> 'val list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val list"
 where
   "exec [] stack env = stack"
 | "exec (instr # instrs) stack env =
     (case instr of
-      Const c => exec instrs (c # stack) env
-    | Load x => exec instrs (env x # stack) env
-    | Apply f => exec instrs (f (hd stack) (hd (tl stack))
+      Const c \<Rightarrow> exec instrs (c # stack) env
+    | Load x \<Rightarrow> exec instrs (env x # stack) env
+    | Apply f \<Rightarrow> exec instrs (f (hd stack) (hd (tl stack))
                    # (tl (tl stack))) env)"
 
-definition execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
+definition execute :: "(('adr, 'val) instr) list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val"
   where "execute instrs env = hd (exec instrs [] env)"
 
 
@@ -78,7 +78,7 @@
 text {* We are ready to define the compilation function of expressions
   to lists of stack machine instructions. *}
 
-primrec compile :: "('adr, 'val) expr => (('adr, 'val) instr) list"
+primrec compile :: "('adr, 'val) expr \<Rightarrow> (('adr, 'val) instr) list"
 where
   "compile (Variable x) = [Load x]"
 | "compile (Constant c) = [Const c]"
@@ -114,11 +114,14 @@
 proof -
   have "\<And>stack. exec (compile e) stack env = eval e env # stack"
   proof (induct e)
-    case Variable show ?case by simp
+    case Variable
+    show ?case by simp
   next
-    case Constant show ?case by simp
+    case Constant
+    show ?case by simp
   next
-    case Binop then show ?case by (simp add: exec_append)
+    case Binop
+    then show ?case by (simp add: exec_append)
   qed
   then show ?thesis by (simp add: execute_def)
 qed
@@ -134,8 +137,10 @@
   "exec (xs @ ys) stack env = exec ys (exec xs stack env) env"
 proof (induct xs arbitrary: stack)
   case (Nil s)
-  have "exec ([] @ ys) s env = exec ys s env" by simp
-  also have "... = exec ys (exec [] s env) env" by simp
+  have "exec ([] @ ys) s env = exec ys s env"
+    by simp
+  also have "\<dots> = exec ys (exec [] s env) env"
+    by simp
   finally show ?case .
 next
   case (Cons x xs s)
@@ -144,22 +149,27 @@
     case (Const val)
     have "exec ((Const val # xs) @ ys) s env = exec (Const val # xs @ ys) s env"
       by simp
-    also have "... = exec (xs @ ys) (val # s) env" by simp
-    also from Cons have "... = exec ys (exec xs (val # s) env) env" .
-    also have "... = exec ys (exec (Const val # xs) s env) env" by simp
+    also have "\<dots> = exec (xs @ ys) (val # s) env"
+      by simp
+    also from Cons have "\<dots> = exec ys (exec xs (val # s) env) env" .
+    also have "\<dots> = exec ys (exec (Const val # xs) s env) env"
+      by simp
     finally show ?case .
   next
     case (Load adr)
-    from Cons show ?case by simp -- {* same as above *}
+    from Cons show ?case
+      by simp -- {* same as above *}
   next
     case (Apply fn)
     have "exec ((Apply fn # xs) @ ys) s env =
         exec (Apply fn # xs @ ys) s env" by simp
-    also have "... =
-        exec (xs @ ys) (fn (hd s) (hd (tl s)) # (tl (tl s))) env" by simp
-    also from Cons have "... =
+    also have "\<dots> =
+        exec (xs @ ys) (fn (hd s) (hd (tl s)) # (tl (tl s))) env"
+      by simp
+    also from Cons have "\<dots> =
         exec ys (exec xs (fn (hd s) (hd (tl s)) # tl (tl s)) env) env" .
-    also have "... = exec ys (exec (Apply fn # xs) s env) env" by simp
+    also have "\<dots> = exec ys (exec (Apply fn # xs) s env) env"
+      by simp
     finally show ?case .
   qed
 qed
@@ -171,8 +181,10 @@
     case (Variable adr s)
     have "exec (compile (Variable adr)) s env = exec [Load adr] s env"
       by simp
-    also have "... = env adr # s" by simp
-    also have "env adr = eval (Variable adr) env" by simp
+    also have "\<dots> = env adr # s"
+      by simp
+    also have "env adr = eval (Variable adr) env"
+      by simp
     finally show ?case .
   next
     case (Constant val s)
@@ -180,15 +192,20 @@
   next
     case (Binop fn e1 e2 s)
     have "exec (compile (Binop fn e1 e2)) s env =
-        exec (compile e2 @ compile e1 @ [Apply fn]) s env" by simp
-    also have "... = exec [Apply fn]
+        exec (compile e2 @ compile e1 @ [Apply fn]) s env"
+      by simp
+    also have "\<dots> = exec [Apply fn]
         (exec (compile e1) (exec (compile e2) s env) env) env"
       by (simp only: exec_append)
-    also have "exec (compile e2) s env = eval e2 env # s" by fact
-    also have "exec (compile e1) ... env = eval e1 env # ..." by fact
-    also have "exec [Apply fn] ... env =
-        fn (hd ...) (hd (tl ...)) # (tl (tl ...))" by simp
-    also have "... = fn (eval e1 env) (eval e2 env) # s" by simp
+    also have "exec (compile e2) s env = eval e2 env # s"
+      by fact
+    also have "exec (compile e1) \<dots> env = eval e1 env # \<dots>"
+      by fact
+    also have "exec [Apply fn] \<dots> env =
+        fn (hd \<dots>) (hd (tl \<dots>)) # (tl (tl \<dots>))"
+      by simp
+    also have "\<dots> = fn (eval e1 env) (eval e2 env) # s"
+      by simp
     also have "fn (eval e1 env) (eval e2 env) =
         eval (Binop fn e1 e2) env"
       by simp
@@ -198,7 +215,8 @@
   have "execute (compile e) env = hd (exec (compile e) [] env)"
     by (simp add: execute_def)
   also from exec_compile have "exec (compile e) [] env = [eval e env]" .
-  also have "hd ... = eval e env" by simp
+  also have "hd \<dots> = eval e env"
+    by simp
   finally show ?thesis .
 qed
 
diff -r e4e8cbd9d780 -r abc140f21caa src/HOL/Isar_Examples/Fibonacci.thy
--- a/src/HOL/Isar_Examples/Fibonacci.thy	Thu Feb 20 23:16:33 2014 +0100
+++ b/src/HOL/Isar_Examples/Fibonacci.thy	Thu Feb 20 23:46:40 2014 +0100
@@ -40,7 +40,8 @@
 text {* Alternative induction rule. *}
 
 theorem fib_induct:
-    "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P (n::nat)"
+  fixes n :: nat
+  shows "P 0 \<Longrightarrow> P 1 \<Longrightarrow> (\<And>n. P (n + 1) \<Longrightarrow> P n \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
   by (induct rule: fib.induct) simp_all
 
 
@@ -77,21 +78,23 @@
   fix n
   have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
     by simp
-  also have "... = fib (n + 2) + fib (n + 1)" by simp
-  also have "gcd (fib (n + 2)) ... = gcd (fib (n + 2)) (fib (n + 1))"
+  also have "\<dots> = fib (n + 2) + fib (n + 1)"
+    by simp
+  also have "gcd (fib (n + 2)) \<dots> = gcd (fib (n + 2)) (fib (n + 1))"
     by (rule gcd_add2_nat)
-  also have "... = gcd (fib (n + 1)) (fib (n + 1 + 1))"
+  also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
     by (simp add: gcd_commute_nat)
-  also assume "... = 1"
+  also assume "\<dots> = 1"
   finally show "?P (n + 2)" .
 qed
 
-lemma gcd_mult_add: "(0::nat) < n ==> gcd (n * k + m) n = gcd m n"
+lemma gcd_mult_add: "(0::nat) < n \<Longrightarrow> gcd (n * k + m) n = gcd m n"
 proof -
   assume "0 < n"
   then have "gcd (n * k + m) n = gcd n (m mod n)"
     by (simp add: gcd_non_0_nat add_commute)
-  also from `0 < n` have "... = gcd m n" by (simp add: gcd_non_0_nat)
+  also from `0 < n` have "\<dots> = gcd m n"
+    by (simp add: gcd_non_0_nat)
   finally show ?thesis .
 qed
 
@@ -106,22 +109,23 @@
   also have "fib (n + k + 1)
       = fib (k + 1) * fib (n + 1) + fib k * fib n"
     by (rule fib_add)
-  also have "gcd ... (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
+  also have "gcd \<dots> (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
     by (simp add: gcd_mult_add)
-  also have "... = gcd (fib n) (fib (k + 1))"
+  also have "\<dots> = gcd (fib n) (fib (k + 1))"
     by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel_nat)
-  also have "... = gcd (fib m) (fib n)"
+  also have "\<dots> = gcd (fib m) (fib n)"
     using Suc by (simp add: gcd_commute_nat)
   finally show ?thesis .
 qed
 
 lemma gcd_fib_diff:
-  assumes "m <= n"
+  assumes "m \<le> n"
   shows "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
 proof -
   have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))"
     by (simp add: gcd_fib_add)
-  also from `m <= n` have "n - m + m = n" by simp
+  also from `m \<le> n` have "n - m + m = n"
+    by simp
   finally show ?thesis .
 qed
 
@@ -134,15 +138,18 @@
   proof -
     have "n mod m = (if n < m then n else (n - m) mod m)"
       by (rule mod_if)
-    also have "gcd (fib m) (fib ...) = gcd (fib m) (fib n)"
+    also have "gcd (fib m) (fib \<dots>) = gcd (fib m) (fib n)"
     proof (cases "n < m")
-      case True then show ?thesis by simp
+      case True
+      then show ?thesis by simp
     next
-      case False then have "m <= n" by simp
-      from `0 < m` and False have "n - m < n" by simp
+      case False
+      then have "m \<le> n" by simp
+      from `0 < m` and False have "n - m < n"
+        by simp
       with hyp have "gcd (fib m) (fib ((n - m) mod m))
           = gcd (fib m) (fib (n - m))" by simp
-      also have "... = gcd (fib m) (fib n)"
+      also have "\<dots> = gcd (fib m) (fib n)"
         using `m <= n` by (rule gcd_fib_diff)
       finally have "gcd (fib m) (fib ((n - m) mod m)) =
           gcd (fib m) (fib n)" .
@@ -154,12 +161,18 @@
 
 theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n")
 proof (induct m n rule: gcd_nat_induct)
-  fix m show "fib (gcd m 0) = gcd (fib m) (fib 0)" by simp
-  fix n :: nat assume n: "0 < n"
-  then have "gcd m n = gcd n (m mod n)" by (simp add: gcd_non_0_nat)
-  also assume hyp: "fib ... = gcd (fib n) (fib (m mod n))"
-  also from n have "... = gcd (fib n) (fib m)" by (rule gcd_fib_mod)
-  also have "... = gcd (fib m) (fib n)" by (rule gcd_commute_nat)
+  fix m
+  show "fib (gcd m 0) = gcd (fib m) (fib 0)"
+    by simp
+  fix n :: nat
+  assume n: "0 < n"
+  then have "gcd m n = gcd n (m mod n)"
+    by (simp add: gcd_non_0_nat)
+  also assume hyp: "fib \<dots> = gcd (fib n) (fib (m mod n))"
+  also from n have "\<dots> = gcd (fib n) (fib m)"
+    by (rule gcd_fib_mod)
+  also have "\<dots> = gcd (fib m) (fib n)"
+    by (rule gcd_commute_nat)
   finally show "fib (gcd m n) = gcd (fib m) (fib n)" .
 qed
 
diff -r e4e8cbd9d780 -r abc140f21caa src/HOL/Isar_Examples/Peirce.thy
--- a/src/HOL/Isar_Examples/Peirce.thy	Thu Feb 20 23:16:33 2014 +0100
+++ b/src/HOL/Isar_Examples/Peirce.thy	Thu Feb 20 23:46:40 2014 +0100
@@ -19,18 +19,18 @@
   there is negation elimination; it holds in intuitionistic logic as
   well.} *}
 
-theorem "((A --> B) --> A) --> A"
+theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
 proof
-  assume "(A --> B) --> A"
+  assume "(A \<longrightarrow> B) \<longrightarrow> A"
   show A
   proof (rule classical)
-    assume "~ A"
-    have "A --> B"
+    assume "\<not> A"
+    have "A \<longrightarrow> B"
     proof
       assume A
-      with `~ A` show B by contradiction
+      with `\<not> A` show B by contradiction
     qed
-    with `(A --> B) --> A` show A ..
+    with `(A \<longrightarrow> B) \<longrightarrow> A` show A ..
   qed
 qed
 
@@ -48,19 +48,19 @@
   contrast, strong assumptions (as introduced by \isacommand{assume})
   are solved immediately. *}
 
-theorem "((A --> B) --> A) --> A"
+theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
 proof
-  assume "(A --> B) --> A"
+  assume "(A \<longrightarrow> B) \<longrightarrow> A"
   show A
   proof (rule classical)
-    presume "A --> B"
-    with `(A --> B) --> A` show A ..
+    presume "A \<longrightarrow> B"
+    with `(A \<longrightarrow> B) \<longrightarrow> A` show A ..
   next
-    assume "~ A"
-    show "A --> B"
+    assume "\<not> A"
+    show "A \<longrightarrow> B"
     proof
       assume A
-      with `~ A` show B by contradiction
+      with `\<not> A` show B by contradiction
     qed
   qed
 qed
diff -r e4e8cbd9d780 -r abc140f21caa src/HOL/Isar_Examples/Summation.thy
--- a/src/HOL/Isar_Examples/Summation.thy	Thu Feb 20 23:16:33 2014 +0100
+++ b/src/HOL/Isar_Examples/Summation.thy	Thu Feb 20 23:46:40 2014 +0100
@@ -26,10 +26,13 @@
 proof (induct n)
   show "?P 0" by simp
 next
-  fix n have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp
+  fix n have "?S (n + 1) = ?S n + 2 * (n + 1)"
+    by simp
   also assume "?S n = n * (n + 1)"
-  also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp
-  finally show "?P (Suc n)" by simp
+  also have "\<dots> + 2 * (n + 1) = (n + 1) * (n + 2)"
+    by simp
+  finally show "?P (Suc n)"
+    by simp
 qed
 
 text {* The above proof is a typical instance of mathematical
@@ -80,10 +83,14 @@
 proof (induct n)
   show "?P 0" by simp
 next
-  fix n have "?S (n + 1) = ?S n + 2 * n + 1" by simp
+  fix n
+  have "?S (n + 1) = ?S n + 2 * n + 1"
+    by simp
   also assume "?S n = n^Suc (Suc 0)"
-  also have "... + 2 * n + 1 = (n + 1)^Suc (Suc 0)" by simp
-  finally show "?P (Suc n)" by simp
+  also have "\<dots> + 2 * n + 1 = (n + 1)^Suc (Suc 0)"
+    by simp
+  finally show "?P (Suc n)"
+    by simp
 qed
 
 text {* Subsequently we require some additional tweaking of Isabelle
@@ -98,12 +105,15 @@
 proof (induct n)
   show "?P 0" by simp
 next
-  fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)"
+  fix n
+  have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)"
     by (simp add: distrib)
   also assume "?S n = n * (n + 1) * (2 * n + 1)"
-  also have "... + 6 * (n + 1)^Suc (Suc 0) =
-      (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib)
-  finally show "?P (Suc n)" by simp
+  also have "\<dots> + 6 * (n + 1)^Suc (Suc 0) =
+      (n + 1) * (n + 2) * (2 * (n + 1) + 1)"
+    by (simp add: distrib)
+  finally show "?P (Suc n)"
+    by simp
 qed
 
 theorem sum_of_cubes:
@@ -112,12 +122,14 @@
 proof (induct n)
   show "?P 0" by (simp add: power_eq_if)
 next
-  fix n have "?S (n + 1) = ?S n + 4 * (n + 1)^3"
+  fix n
+  have "?S (n + 1) = ?S n + 4 * (n + 1)^3"
     by (simp add: power_eq_if distrib)
   also assume "?S n = (n * (n + 1))^Suc (Suc 0)"
-  also have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)"
+  also have "\<dots> + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)"
     by (simp add: power_eq_if distrib)
-  finally show "?P (Suc n)" by simp
+  finally show "?P (Suc n)"
+    by simp
 qed
 
 text {* Note that in contrast to older traditions of tactical proof