# HG changeset patch
# User wenzelm
# Date 1416664624 -3600
# Node ID 4c3bb56b8ce754132122f31df71018e89ea7dff7
# Parent  67baff6f697cd4d619c66dbf53e44915d9196dc1
misc tuning and modernization;

diff -r 67baff6f697c -r 4c3bb56b8ce7 src/HOL/ex/Abstract_NAT.thy
--- a/src/HOL/ex/Abstract_NAT.thy	Sat Nov 22 14:13:36 2014 +0100
+++ b/src/HOL/ex/Abstract_NAT.thy	Sat Nov 22 14:57:04 2014 +0100
@@ -2,18 +2,18 @@
     Author:     Makarius
 *)
 
-section {* Abstract Natural Numbers primitive recursion *}
+section \<open>Abstract Natural Numbers primitive recursion\<close>
 
 theory Abstract_NAT
 imports Main
 begin
 
-text {* Axiomatic Natural Numbers (Peano) -- a monomorphic theory. *}
+text \<open>Axiomatic Natural Numbers (Peano) -- a monomorphic theory.\<close>
 
 locale NAT =
   fixes zero :: 'n
     and succ :: "'n \<Rightarrow> 'n"
-  assumes succ_inject [simp]: "(succ m = succ n) = (m = n)"
+  assumes succ_inject [simp]: "succ m = succ n \<longleftrightarrow> m = n"
     and succ_neq_zero [simp]: "succ m \<noteq> zero"
     and induct [case_names zero succ, induct type: 'n]:
       "P zero \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (succ n)) \<Longrightarrow> P n"
@@ -23,7 +23,7 @@
   by (rule succ_neq_zero [symmetric])
 
 
-text {* \medskip Primitive recursion as a (functional) relation -- polymorphic! *}
+text \<open>\medskip Primitive recursion as a (functional) relation -- polymorphic!\<close>
 
 inductive Rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a \<Rightarrow> bool"
   for e :: 'a and r :: "'n \<Rightarrow> 'a \<Rightarrow> 'a"
@@ -47,7 +47,7 @@
     qed
   next
     case (succ m)
-    from `\<exists>!y. ?R m y`
+    from \<open>\<exists>!y. ?R m y\<close>
     obtain y where y: "?R m y"
       and yy': "\<And>y'. ?R m y' \<Longrightarrow> y = y'" by blast
     show "\<exists>!z. ?R (succ m) z"
@@ -61,7 +61,7 @@
 qed
 
 
-text {* \medskip The recursion operator -- polymorphic! *}
+text \<open>\medskip The recursion operator -- polymorphic!\<close>
 
 definition rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a"
   where "rec e r x = (THE y. Rec e r x y)"
@@ -86,7 +86,7 @@
 qed
 
 
-text {* \medskip Example: addition (monomorphic) *}
+text \<open>\medskip Example: addition (monomorphic)\<close>
 
 definition add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n"
   where "add m n = rec n (\<lambda>_ k. succ k) m"
@@ -109,7 +109,7 @@
   by simp
 
 
-text {* \medskip Example: replication (polymorphic) *}
+text \<open>\medskip Example: replication (polymorphic)\<close>
 
 definition repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list"
   where "repl n x = rec [] (\<lambda>_ xs. x # xs) n"
@@ -124,12 +124,12 @@
 end
 
 
-text {* \medskip Just see that our abstract specification makes sense \dots *}
+text \<open>\medskip Just see that our abstract specification makes sense \dots\<close>
 
 interpretation NAT 0 Suc
 proof (rule NAT.intro)
   fix m n
-  show "(Suc m = Suc n) = (m = n)" by simp
+  show "Suc m = Suc n \<longleftrightarrow> m = n" by simp
   show "Suc m \<noteq> 0" by simp
   fix P
   assume zero: "P 0"
diff -r 67baff6f697c -r 4c3bb56b8ce7 src/HOL/ex/Antiquote.thy
--- a/src/HOL/ex/Antiquote.thy	Sat Nov 22 14:13:36 2014 +0100
+++ b/src/HOL/ex/Antiquote.thy	Sat Nov 22 14:57:04 2014 +0100
@@ -2,16 +2,13 @@
     Author:     Markus Wenzel, TU Muenchen
 *)
 
-section {* Antiquotations *}
+section \<open>Antiquotations\<close>
 
 theory Antiquote
 imports Main
 begin
 
-text {*
-  A simple example on quote / antiquote in higher-order abstract
-  syntax.
-*}
+text \<open>A simple example on quote / antiquote in higher-order abstract syntax.\<close>
 
 definition var :: "'a \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat"  ("VAR _" [1000] 999)
   where "var x env = env x"
@@ -22,23 +19,21 @@
 syntax
   "_Expr" :: "'a \<Rightarrow> 'a"  ("EXPR _" [1000] 999)
 
-parse_translation {*
-  [Syntax_Trans.quote_antiquote_tr
-    @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
-*}
+parse_translation
+  \<open>[Syntax_Trans.quote_antiquote_tr
+    @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]\<close>
 
-print_translation {*
-  [Syntax_Trans.quote_antiquote_tr'
-    @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
-*}
+print_translation
+  \<open>[Syntax_Trans.quote_antiquote_tr'
+    @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]\<close>
 
 term "EXPR (a + b + c)"
 term "EXPR (a + b + c + VAR x + VAR y + 1)"
 term "EXPR (VAR (f w) + VAR x)"
 
-term "Expr (\<lambda>env. env x)"    -- {* improper *}
+term "Expr (\<lambda>env. env x)"    -- \<open>improper\<close>
 term "Expr (\<lambda>env. f env)"
-term "Expr (\<lambda>env. f env + env x)"    -- {* improper *}
+term "Expr (\<lambda>env. f env + env x)"    -- \<open>improper\<close>
 term "Expr (\<lambda>env. f env y z)"
 term "Expr (\<lambda>env. f env + g y env)"
 term "Expr (\<lambda>env. f env + g env y + h a env z)"
diff -r 67baff6f697c -r 4c3bb56b8ce7 src/HOL/ex/Guess.thy
--- a/src/HOL/ex/Guess.thy	Sat Nov 22 14:13:36 2014 +0100
+++ b/src/HOL/ex/Guess.thy	Sat Nov 22 14:57:04 2014 +0100
@@ -8,9 +8,8 @@
 imports Main
 begin
 
-lemma True
-proof
-
+notepad
+begin
   have 1: "\<exists>x. x = x" by simp
 
   from 1 guess ..
@@ -18,13 +17,12 @@
   from 1 guess x :: 'a ..
   from 1 guess x :: nat ..
 
-  have 2: "\<exists>x y. x = x & y = y" by simp
+  have 2: "\<exists>x y. x = x \<and> y = y" by simp
   from 2 guess apply - apply (erule exE conjE)+ done
   from 2 guess x apply - apply (erule exE conjE)+ done
   from 2 guess x y apply - apply (erule exE conjE)+ done
   from 2 guess x :: 'a and y :: 'b apply - apply (erule exE conjE)+ done
   from 2 guess x y :: nat apply - apply (erule exE conjE)+ done
-
-qed
+end
 
 end
diff -r 67baff6f697c -r 4c3bb56b8ce7 src/HOL/ex/Hebrew.thy
--- a/src/HOL/ex/Hebrew.thy	Sat Nov 22 14:13:36 2014 +0100
+++ b/src/HOL/ex/Hebrew.thy	Sat Nov 22 14:57:04 2014 +0100
@@ -4,13 +4,13 @@
 formal and informal ones.
 *)
 
-section {* A Hebrew theory *}
+section \<open>A Hebrew theory\<close>
 
 theory Hebrew
 imports Main
 begin
 
-text {* The Hebrew Alef-Bet (א-ב). *}
+text \<open>The Hebrew Alef-Bet (א-ב).\<close>
 
 datatype alef_bet =
     Alef    ("א")
@@ -39,9 +39,10 @@
 thm alef_bet.induct
 
 
-text {* Interpreting Hebrew letters as numbers. *}
+text \<open>Interpreting Hebrew letters as numbers.\<close>
 
-primrec mispar :: "alef_bet => nat" where
+primrec mispar :: "alef_bet => nat"
+where
   "mispar א = 1"
 | "mispar ב = 2"
 | "mispar ג = 3"
diff -r 67baff6f697c -r 4c3bb56b8ce7 src/HOL/ex/Higher_Order_Logic.thy
--- a/src/HOL/ex/Higher_Order_Logic.thy	Sat Nov 22 14:13:36 2014 +0100
+++ b/src/HOL/ex/Higher_Order_Logic.thy	Sat Nov 22 14:57:04 2014 +0100
@@ -2,21 +2,21 @@
     Author:     Gertrud Bauer and Markus Wenzel, TU Muenchen
 *)
 
-section {* Foundations of HOL *}
+section \<open>Foundations of HOL\<close>
 
 theory Higher_Order_Logic imports Pure begin
 
-text {*
+text \<open>
   The following theory development demonstrates Higher-Order Logic
   itself, represented directly within the Pure framework of Isabelle.
   The ``HOL'' logic given here is essentially that of Gordon
   @{cite "Gordon:1985:HOL"}, although we prefer to present basic concepts
   in a slightly more conventional manner oriented towards plain
   Natural Deduction.
-*}
+\<close>
 
 
-subsection {* Pure Logic *}
+subsection \<open>Pure Logic\<close>
 
 class type
 default_sort type
@@ -26,7 +26,7 @@
 instance "fun" :: (type, type) type ..
 
 
-subsubsection {* Basic logical connectives *}
+subsubsection \<open>Basic logical connectives\<close>
 
 judgment
   Trueprop :: "o \<Rightarrow> prop"    ("_" 5)
@@ -41,7 +41,7 @@
   allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
 
 
-subsubsection {* Extensional equality *}
+subsubsection \<open>Extensional equality\<close>
 
 axiomatization
   equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infixl "=" 50)
@@ -75,35 +75,26 @@
   by (rule subst) (rule sym)
 
 
-subsubsection {* Derived connectives *}
+subsubsection \<open>Derived connectives\<close>
 
-definition
-  false :: o  ("\<bottom>") where
-  "\<bottom> \<equiv> \<forall>A. A"
+definition false :: o  ("\<bottom>") where "\<bottom> \<equiv> \<forall>A. A"
 
-definition
-  true :: o  ("\<top>") where
-  "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
+definition true :: o  ("\<top>") where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
 
-definition
-  not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40) where
-  "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>"
+definition not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40)
+  where "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>"
 
-definition
-  conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35) where
-  "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
+definition conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35)
+  where "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
 
-definition
-  disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30) where
-  "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
+definition disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30)
+  where "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
 
-definition
-  Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10) where
-  "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
+definition Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
+  where "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
 
-abbreviation
-  not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "\<noteq>" 50) where
-  "x \<noteq> y \<equiv> \<not> (x = y)"
+abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "\<noteq>" 50)
+  where "x \<noteq> y \<equiv> \<not> (x = y)"
 
 theorem falseE [elim]: "\<bottom> \<Longrightarrow> A"
 proof (unfold false_def)
@@ -133,7 +124,7 @@
 lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
   by (rule notE)
 
-lemmas contradiction = notE notE'  -- {* proof by contradiction in any order *}
+lemmas contradiction = notE notE'  -- \<open>proof by contradiction in any order\<close>
 
 theorem conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
 proof (unfold conj_def)
@@ -143,8 +134,8 @@
     fix C show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
     proof
       assume "A \<longrightarrow> B \<longrightarrow> C"
-      also note `A`
-      also note `B`
+      also note \<open>A\<close>
+      also note \<open>B\<close>
       finally show C .
     qed
   qed
@@ -180,7 +171,7 @@
     fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
     proof
       assume "A \<longrightarrow> C"
-      also note `A`
+      also note \<open>A\<close>
       finally have C .
       then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
     qed
@@ -197,7 +188,7 @@
       show "(B \<longrightarrow> C) \<longrightarrow> C"
       proof
         assume "B \<longrightarrow> C"
-        also note `B`
+        also note \<open>B\<close>
         finally show C .
       qed
     qed
@@ -229,7 +220,7 @@
     proof
       assume "\<forall>x. P x \<longrightarrow> C"
       then have "P a \<longrightarrow> C" ..
-      also note `P a`
+      also note \<open>P a\<close>
       finally show C .
     qed
   qed
@@ -252,7 +243,7 @@
 qed
 
 
-subsection {* Classical logic *}
+subsection \<open>Classical logic\<close>
 
 locale classical =
   assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
@@ -267,7 +258,7 @@
     have "A \<longrightarrow> B"
     proof
       assume A
-      with `\<not> A` show B by (rule contradiction)
+      with \<open>\<not> A\<close> show B by (rule contradiction)
     qed
     with a show A ..
   qed
@@ -280,7 +271,7 @@
   show A
   proof (rule classical)
     assume "\<not> A"
-    with `\<not> \<not> A` show ?thesis by (rule contradiction)
+    with \<open>\<not> \<not> A\<close> show ?thesis by (rule contradiction)
   qed
 qed
 
@@ -293,10 +284,10 @@
     have "\<not> A"
     proof
       assume A then have "A \<or> \<not> A" ..
-      with `\<not> (A \<or> \<not> A)` show \<bottom> by (rule contradiction)
+      with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction)
     qed
     then have "A \<or> \<not> A" ..
-    with `\<not> (A \<or> \<not> A)` show \<bottom> by (rule contradiction)
+    with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction)
   qed
 qed
 
diff -r 67baff6f697c -r 4c3bb56b8ce7 src/HOL/ex/Multiquote.thy
--- a/src/HOL/ex/Multiquote.thy	Sat Nov 22 14:13:36 2014 +0100
+++ b/src/HOL/ex/Multiquote.thy	Sat Nov 22 14:57:04 2014 +0100
@@ -2,22 +2,22 @@
     Author:     Markus Wenzel, TU Muenchen
 *)
 
-section {* Multiple nested quotations and anti-quotations *}
+section \<open>Multiple nested quotations and anti-quotations\<close>
 
 theory Multiquote
 imports Main
 begin
 
-text {*
+text \<open>
   Multiple nested quotations and anti-quotations -- basically a
   generalized version of de-Bruijn representation.
-*}
+\<close>
 
 syntax
   "_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"    ("\<guillemotleft>_\<guillemotright>" [0] 1000)
   "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"    ("\<acute>_" [1000] 1000)
 
-parse_translation {*
+parse_translation \<open>
   let
     fun antiquote_tr i (Const (@{syntax_const "_antiquote"}, _) $
           (t as Const (@{syntax_const "_antiquote"}, _) $ _)) = skip_antiquote_tr i t
@@ -33,15 +33,15 @@
     fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
       | quote_tr ts = raise TERM ("quote_tr", ts);
   in [(@{syntax_const "_quote"}, K quote_tr)] end
-*}
+\<close>
 
-text {* basic examples *}
+text \<open>basic examples\<close>
 term "\<guillemotleft>a + b + c\<guillemotright>"
 term "\<guillemotleft>a + b + c + \<acute>x + \<acute>y + 1\<guillemotright>"
 term "\<guillemotleft>\<acute>(f w) + \<acute>x\<guillemotright>"
 term "\<guillemotleft>f \<acute>x \<acute>y z\<guillemotright>"
 
-text {* advanced examples *}
+text \<open>advanced examples\<close>
 term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright>\<guillemotright>"
 term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright> \<circ> \<acute>f\<guillemotright>"
 term "\<guillemotleft>\<acute>(f \<circ> \<acute>g)\<guillemotright>"
diff -r 67baff6f697c -r 4c3bb56b8ce7 src/HOL/ex/PER.thy
--- a/src/HOL/ex/PER.thy	Sat Nov 22 14:13:36 2014 +0100
+++ b/src/HOL/ex/PER.thy	Sat Nov 22 14:57:04 2014 +0100
@@ -2,11 +2,13 @@
     Author:     Oscar Slotosch and Markus Wenzel, TU Muenchen
 *)
 
-section {* Partial equivalence relations *}
+section \<open>Partial equivalence relations\<close>
 
-theory PER imports Main begin
+theory PER
+imports Main
+begin
 
-text {*
+text \<open>
   Higher-order quotients are defined over partial equivalence
   relations (PERs) instead of total ones.  We provide axiomatic type
   classes @{text "equiv < partial_equiv"} and a type constructor
@@ -17,41 +19,41 @@
   Implementation in Isabelle HOL.}  Elsa L. Gunter and Amy Felty,
   editors, Theorem Proving in Higher Order Logics: TPHOLs '97,
   Springer LNCS 1275, 1997.
-*}
+\<close>
 
 
-subsection {* Partial equivalence *}
+subsection \<open>Partial equivalence\<close>
 
-text {*
+text \<open>
   Type class @{text partial_equiv} models partial equivalence
-  relations (PERs) using the polymorphic @{text "\<sim> :: 'a => 'a =>
+  relations (PERs) using the polymorphic @{text "\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow>
   bool"} relation, which is required to be symmetric and transitive,
   but not necessarily reflexive.
-*}
+\<close>
 
 class partial_equiv =
-  fixes eqv :: "'a => 'a => bool"    (infixl "\<sim>" 50)
-  assumes partial_equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
-  assumes partial_equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
+  fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<sim>" 50)
+  assumes partial_equiv_sym [elim?]: "x \<sim> y \<Longrightarrow> y \<sim> x"
+  assumes partial_equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z"
 
-text {*
+text \<open>
   \medskip The domain of a partial equivalence relation is the set of
   reflexive elements.  Due to symmetry and transitivity this
   characterizes exactly those elements that are connected with
   \emph{any} other one.
-*}
+\<close>
 
 definition
   "domain" :: "'a::partial_equiv set" where
   "domain = {x. x \<sim> x}"
 
-lemma domainI [intro]: "x \<sim> x ==> x \<in> domain"
+lemma domainI [intro]: "x \<sim> x \<Longrightarrow> x \<in> domain"
   unfolding domain_def by blast
 
-lemma domainD [dest]: "x \<in> domain ==> x \<sim> x"
+lemma domainD [dest]: "x \<in> domain \<Longrightarrow> x \<sim> x"
   unfolding domain_def by blast
 
-theorem domainI' [elim?]: "x \<sim> y ==> x \<in> domain"
+theorem domainI' [elim?]: "x \<sim> y \<Longrightarrow> x \<in> domain"
 proof
   assume xy: "x \<sim> y"
   also from xy have "y \<sim> x" ..
@@ -59,35 +61,34 @@
 qed
 
 
-subsection {* Equivalence on function spaces *}
+subsection \<open>Equivalence on function spaces\<close>
 
-text {*
+text \<open>
   The @{text \<sim>} relation is lifted to function spaces.  It is
   important to note that this is \emph{not} the direct product, but a
   structural one corresponding to the congruence property.
-*}
+\<close>
 
 instantiation "fun" :: (partial_equiv, partial_equiv) partial_equiv
 begin
 
-definition
-  eqv_fun_def: "f \<sim> g == \<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y --> f x \<sim> g y"
+definition "f \<sim> g \<longleftrightarrow> (\<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y \<longrightarrow> f x \<sim> g y)"
 
 lemma partial_equiv_funI [intro?]:
-    "(!!x y. x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y) ==> f \<sim> g"
+    "(\<And>x y. x \<in> domain \<Longrightarrow> y \<in> domain \<Longrightarrow> x \<sim> y \<Longrightarrow> f x \<sim> g y) \<Longrightarrow> f \<sim> g"
   unfolding eqv_fun_def by blast
 
 lemma partial_equiv_funD [dest?]:
-    "f \<sim> g ==> x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y"
+    "f \<sim> g \<Longrightarrow> x \<in> domain \<Longrightarrow> y \<in> domain \<Longrightarrow> x \<sim> y \<Longrightarrow> f x \<sim> g y"
   unfolding eqv_fun_def by blast
 
-text {*
+text \<open>
   The class of partial equivalence relations is closed under function
   spaces (in \emph{both} argument positions).
-*}
+\<close>
 
 instance proof
-  fix f g h :: "'a::partial_equiv => 'b::partial_equiv"
+  fix f g h :: "'a::partial_equiv \<Rightarrow> 'b::partial_equiv"
   assume fg: "f \<sim> g"
   show "g \<sim> f"
   proof
@@ -112,29 +113,29 @@
 end
 
 
-subsection {* Total equivalence *}
+subsection \<open>Total equivalence\<close>
 
-text {*
+text \<open>
   The class of total equivalence relations on top of PERs.  It
   coincides with the standard notion of equivalence, i.e.\ @{text "\<sim>
-  :: 'a => 'a => bool"} is required to be reflexive, transitive and
+  :: 'a \<Rightarrow> 'a \<Rightarrow> bool"} is required to be reflexive, transitive and
   symmetric.
-*}
+\<close>
 
 class equiv =
   assumes eqv_refl [intro]: "x \<sim> x"
 
-text {*
+text \<open>
   On total equivalences all elements are reflexive, and congruence
   holds unconditionally.
-*}
+\<close>
 
 theorem equiv_domain [intro]: "(x::'a::equiv) \<in> domain"
 proof
   show "x \<sim> x" ..
 qed
 
-theorem equiv_cong [dest?]: "f \<sim> g ==> x \<sim> y ==> f x \<sim> g (y::'a::equiv)"
+theorem equiv_cong [dest?]: "f \<sim> g \<Longrightarrow> x \<sim> y \<Longrightarrow> f x \<sim> g (y::'a::equiv)"
 proof -
   assume "f \<sim> g"
   moreover have "x \<in> domain" ..
@@ -144,12 +145,12 @@
 qed
 
 
-subsection {* Quotient types *}
+subsection \<open>Quotient types\<close>
 
-text {*
+text \<open>
   The quotient type @{text "'a quot"} consists of all
   \emph{equivalence classes} over elements of the base type @{typ 'a}.
-*}
+\<close>
 
 definition "quot = {{x. a \<sim> x}| a::'a::partial_equiv. True}"
 
@@ -159,17 +160,16 @@
 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
   unfolding quot_def by blast
 
-lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"
+lemma quotE [elim]: "R \<in> quot \<Longrightarrow> (\<And>a. R = {x. a \<sim> x} \<Longrightarrow> C) \<Longrightarrow> C"
   unfolding quot_def by blast
 
-text {*
+text \<open>
   \medskip Abstracted equivalence classes are the canonical
   representation of elements of a quotient type.
-*}
+\<close>
 
-definition
-  eqv_class :: "('a::partial_equiv) => 'a quot"    ("\<lfloor>_\<rfloor>") where
-  "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
+definition eqv_class :: "('a::partial_equiv) \<Rightarrow> 'a quot"  ("\<lfloor>_\<rfloor>")
+  where "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
 
 theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>"
 proof (cases A)
@@ -184,19 +184,19 @@
   using quot_rep by blast
 
 
-subsection {* Equality on quotients *}
+subsection \<open>Equality on quotients\<close>
 
-text {*
+text \<open>
   Equality of canonical quotient elements corresponds to the original
   relation as follows.
-*}
+\<close>
 
-theorem eqv_class_eqI [intro]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
+theorem eqv_class_eqI [intro]: "a \<sim> b \<Longrightarrow> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
 proof -
   assume ab: "a \<sim> b"
   have "{x. a \<sim> x} = {x. b \<sim> x}"
   proof (rule Collect_cong)
-    fix x show "(a \<sim> x) = (b \<sim> x)"
+    fix x show "a \<sim> x \<longleftrightarrow> b \<sim> x"
     proof
       from ab have "b \<sim> a" ..
       also assume "a \<sim> x"
@@ -210,7 +210,7 @@
   then show ?thesis by (simp only: eqv_class_def)
 qed
 
-theorem eqv_class_eqD' [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<in> domain ==> a \<sim> b"
+theorem eqv_class_eqD' [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> \<Longrightarrow> a \<in> domain \<Longrightarrow> a \<sim> b"
 proof (unfold eqv_class_def)
   assume "Abs_quot {x. a \<sim> x} = Abs_quot {x. b \<sim> x}"
   then have "{x. a \<sim> x} = {x. b \<sim> x}" by (simp only: Abs_quot_inject quotI)
@@ -220,25 +220,24 @@
   then show "a \<sim> b" ..
 qed
 
-theorem eqv_class_eqD [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<sim> (b::'a::equiv)"
+theorem eqv_class_eqD [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> \<Longrightarrow> a \<sim> (b::'a::equiv)"
 proof (rule eqv_class_eqD')
   show "a \<in> domain" ..
 qed
 
-lemma eqv_class_eq' [simp]: "a \<in> domain ==> (\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
+lemma eqv_class_eq' [simp]: "a \<in> domain \<Longrightarrow> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> \<longleftrightarrow> a \<sim> b"
   using eqv_class_eqI eqv_class_eqD' by (blast del: eqv_refl)
 
-lemma eqv_class_eq [simp]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> (b::'a::equiv))"
+lemma eqv_class_eq [simp]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> \<longleftrightarrow> a \<sim> (b::'a::equiv)"
   using eqv_class_eqI eqv_class_eqD by blast
 
 
-subsection {* Picking representing elements *}
+subsection \<open>Picking representing elements\<close>
 
-definition
-  pick :: "'a::partial_equiv quot => 'a" where
-  "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
+definition pick :: "'a::partial_equiv quot \<Rightarrow> 'a"
+  where "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
 
-theorem pick_eqv' [intro?, simp]: "a \<in> domain ==> pick \<lfloor>a\<rfloor> \<sim> a"
+theorem pick_eqv' [intro?, simp]: "a \<in> domain \<Longrightarrow> pick \<lfloor>a\<rfloor> \<sim> a"
 proof (unfold pick_def)
   assume a: "a \<in> domain"
   show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a"
diff -r 67baff6f697c -r 4c3bb56b8ce7 src/HOL/ex/Sqrt.thy
--- a/src/HOL/ex/Sqrt.thy	Sat Nov 22 14:13:36 2014 +0100
+++ b/src/HOL/ex/Sqrt.thy	Sat Nov 22 14:57:04 2014 +0100
@@ -2,19 +2,19 @@
     Author:     Markus Wenzel, Tobias Nipkow, TU Muenchen
 *)
 
-section {*  Square roots of primes are irrational *}
+section \<open>Square roots of primes are irrational\<close>
 
 theory Sqrt
 imports Complex_Main "~~/src/HOL/Number_Theory/Primes"
 begin
 
-text {* The square root of any prime number (including 2) is irrational. *}
+text \<open>The square root of any prime number (including 2) is irrational.\<close>
 
 theorem sqrt_prime_irrational:
   assumes "prime (p::nat)"
   shows "sqrt p \<notin> \<rat>"
 proof
-  from `prime p` have p: "1 < p" by (simp add: prime_nat_def)
+  from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_nat_def)
   assume "sqrt p \<in> \<rat>"
   then obtain m n :: nat where
       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
@@ -31,12 +31,12 @@
   have "p dvd m \<and> p dvd n"
   proof
     from eq have "p dvd m\<^sup>2" ..
-    with `prime p` show "p dvd m" by (rule prime_dvd_power_nat)
+    with \<open>prime p\<close> show "p dvd m" by (rule prime_dvd_power_nat)
     then obtain k where "m = p * k" ..
     with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square ac_simps)
     with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
     then have "p dvd n\<^sup>2" ..
-    with `prime p` show "p dvd n" by (rule prime_dvd_power_nat)
+    with \<open>prime p\<close> show "p dvd n" by (rule prime_dvd_power_nat)
   qed
   then have "p dvd gcd m n" ..
   with gcd have "p dvd 1" by simp
@@ -47,19 +47,20 @@
 corollary sqrt_2_not_rat: "sqrt 2 \<notin> \<rat>"
   using sqrt_prime_irrational[of 2] by simp
 
-subsection {* Variations *}
 
-text {*
+subsection \<open>Variations\<close>
+
+text \<open>
   Here is an alternative version of the main proof, using mostly
   linear forward-reasoning.  While this results in less top-down
   structure, it is probably closer to proofs seen in mathematics.
-*}
+\<close>
 
 theorem
   assumes "prime (p::nat)"
   shows "sqrt p \<notin> \<rat>"
 proof
-  from `prime p` have p: "1 < p" by (simp add: prime_nat_def)
+  from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_nat_def)
   assume "sqrt p \<in> \<rat>"
   then obtain m n :: nat where
       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
@@ -71,12 +72,12 @@
   also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp
   finally have eq: "m\<^sup>2 = p * n\<^sup>2" ..
   then have "p dvd m\<^sup>2" ..
-  with `prime p` have dvd_m: "p dvd m" by (rule prime_dvd_power_nat)
+  with \<open>prime p\<close> have dvd_m: "p dvd m" by (rule prime_dvd_power_nat)
   then obtain k where "m = p * k" ..
   with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square ac_simps)
   with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
   then have "p dvd n\<^sup>2" ..
-  with `prime p` have "p dvd n" by (rule prime_dvd_power_nat)
+  with \<open>prime p\<close> have "p dvd n" by (rule prime_dvd_power_nat)
   with dvd_m have "p dvd gcd m n" by (rule gcd_greatest_nat)
   with gcd have "p dvd 1" by simp
   then have "p \<le> 1" by (simp add: dvd_imp_le)
@@ -84,9 +85,9 @@
 qed
 
 
-text {* Another old chestnut, which is a consequence of the irrationality of 2. *}
+text \<open>Another old chestnut, which is a consequence of the irrationality of 2.\<close>
 
-lemma "\<exists>a b::real. a \<notin> \<rat> \<and> b \<notin> \<rat> \<and> a powr b \<in> \<rat>" (is "EX a b. ?P a b")
+lemma "\<exists>a b::real. a \<notin> \<rat> \<and> b \<notin> \<rat> \<and> a powr b \<in> \<rat>" (is "\<exists>a b. ?P a b")
 proof cases
   assume "sqrt 2 powr sqrt 2 \<in> \<rat>"
   then have "?P (sqrt 2) (sqrt 2)"