diff -r 7fb5b7dc8332 -r 1e7ccd864b62 src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Sat Jun 20 16:23:56 2015 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Sat Jun 20 16:31:44 2015 +0200
@@ -5,13 +5,13 @@
 in normal form, the cring method is complete.
 *)
 
-section {* Proof of the relative completeness of method comm-ring *}
+section \<open>Proof of the relative completeness of method comm-ring\<close>
 
 theory Commutative_Ring_Complete
 imports Commutative_Ring
 begin
 
-text {* Formalization of normal form *}
+text \<open>Formalization of normal form\<close>
 fun isnorm :: "'a::comm_ring pol \<Rightarrow> bool"
 where
   "isnorm (Pc c) \<longleftrightarrow> True"
@@ -101,7 +101,7 @@
     by (cases x) auto
 qed
 
-text {* mkPX conserves normalizedness (@{text "_cn"}) *}
+text \<open>mkPX conserves normalizedness (@{text "_cn"})\<close>
 lemma mkPX_cn:
   assumes "x \<noteq> 0"
     and "isnorm P"
@@ -125,7 +125,7 @@
     by (cases x) (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
 qed
 
-text {* add conserves normalizedness *}
+text \<open>add conserves normalizedness\<close>
 lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
 proof (induct P Q rule: add.induct)
   case (2 c i P2)
@@ -164,7 +164,7 @@
     from 6 have "isnorm P2" "isnorm Q2"
       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
     moreover
-    from 6 `x < y` y have "isnorm (Pinj d Q2)"
+    from 6 \<open>x < y\<close> y have "isnorm (Pinj d Q2)"
       by (cases d, simp, cases Q2, auto)
     ultimately have ?case by (simp add: mkPinj_cn)
   }
@@ -188,7 +188,7 @@
     from 6 have "isnorm P2" "isnorm Q2"
       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
     moreover
-    from 6 `x > y` x have "isnorm (Pinj d P2)"
+    from 6 \<open>x > y\<close> x have "isnorm (Pinj d P2)"
       by (cases d) (simp, cases P2, auto)
     ultimately have ?case by (simp add: mkPinj_cn)
   }
@@ -204,8 +204,8 @@
     assume "x = 1"
     from 7 have "isnorm R" "isnorm P2"
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 7 `x = 1` have "isnorm (R \<oplus> P2)" by simp
-    with 7 `x = 1` have ?case
+    with 7 \<open>x = 1\<close> have "isnorm (R \<oplus> P2)" by simp
+    with 7 \<open>x = 1\<close> have ?case
       by (simp add: norm_PXtrans[of Q2 y _])
   }
   moreover {
@@ -215,7 +215,7 @@
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
     with 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
     with 7 X NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
-    with `isnorm (PX Q2 y R)` X have ?case
+    with \<open>isnorm (PX Q2 y R)\<close> X have ?case
       by (simp add: norm_PXtrans[of Q2 y _])
   }
   ultimately show ?case by blast
@@ -231,9 +231,9 @@
     assume "x = 1"
     with 8 have "isnorm R" "isnorm P2"
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 8 `x = 1` have "isnorm (R \<oplus> P2)"
+    with 8 \<open>x = 1\<close> have "isnorm (R \<oplus> P2)"
       by simp
-    with 8 `x = 1` have ?case
+    with 8 \<open>x = 1\<close> have ?case
       by (simp add: norm_PXtrans[of Q2 y _])
   }
   moreover {
@@ -244,9 +244,9 @@
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
     with 8 X have "isnorm (Pinj (x - 1) P2)"
       by (cases P2) auto
-    with 8 `x > 1` NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
+    with 8 \<open>x > 1\<close> NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
       by simp
-    with `isnorm (PX Q2 y R)` X have ?case
+    with \<open>isnorm (PX Q2 y R)\<close> X have ?case
       by (simp add: norm_PXtrans[of Q2 y _])
   }
   ultimately show ?case by blast
@@ -288,7 +288,7 @@
     assume "x = y"
     with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)"
       by auto
-    with `x = y` Y0 have ?case
+    with \<open>x = y\<close> Y0 have ?case
       by (simp add: mkPX_cn)
   }
   moreover {
@@ -319,7 +319,7 @@
   ultimately show ?case by blast
 qed simp
 
-text {* mul concerves normalizedness *}
+text \<open>mul concerves normalizedness\<close>
 lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
 proof (induct P Q rule: mul.induct)
   case (2 c i P2)
@@ -357,7 +357,7 @@
     from 6 have "isnorm P2" "isnorm Q2"
       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
     moreover
-    from 6 `x < y` y have "isnorm (Pinj d Q2)"
+    from 6 \<open>x < y\<close> y have "isnorm (Pinj d Q2)"
       by (cases d) (simp, cases Q2, auto)
     ultimately have ?case by (simp add: mkPinj_cn)
   }
@@ -386,7 +386,7 @@
     from 6 have "isnorm P2" "isnorm Q2"
       by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
     moreover
-    from 6 `x > y` x have "isnorm (Pinj d P2)"
+    from 6 \<open>x > y\<close> x have "isnorm (Pinj d P2)"
       by (cases d) (simp, cases P2, auto)
     ultimately have ?case by (simp add: mkPinj_cn)
   }
@@ -404,9 +404,9 @@
     assume "x = 1"
     from 7 have "isnorm R" "isnorm P2"
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 7 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2"
+    with 7 \<open>x = 1\<close> have "isnorm (R \<otimes> P2)" "isnorm Q2"
       by (auto simp add: norm_PX1[of Q2 y R])
-    with 7 `x = 1` Y0 have ?case
+    with 7 \<open>x = 1\<close> Y0 have ?case
       by (simp add: mkPX_cn)
   }
   moreover {
@@ -444,9 +444,9 @@
     assume "x = 1"
     from 8 have "isnorm R" "isnorm P2"
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 8 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2"
+    with 8 \<open>x = 1\<close> have "isnorm (R \<otimes> P2)" "isnorm Q2"
       by (auto simp add: norm_PX1[of Q2 y R])
-    with 8 `x = 1` Y0 have ?case
+    with 8 \<open>x = 1\<close> Y0 have ?case
       by (simp add: mkPX_cn)
   }
   moreover {
@@ -490,7 +490,7 @@
   then show ?case by (simp add: add_cn)
 qed simp
 
-text {* neg conserves normalizedness *}
+text \<open>neg conserves normalizedness\<close>
 lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
 proof (induct P)
   case (Pinj i P2)
@@ -514,11 +514,11 @@
   qed (cases x, auto)
 qed simp
 
-text {* sub conserves normalizedness *}
+text \<open>sub conserves normalizedness\<close>
 lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
   by (simp add: sub_def add_cn neg_cn)
 
-text {* sqr conserves normalizizedness *}
+text \<open>sqr conserves normalizizedness\<close>
 lemma sqr_cn: "isnorm P \<Longrightarrow> isnorm (sqr P)"
 proof (induct P)
   case Pc
@@ -538,7 +538,7 @@
     by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
 qed
 
-text {* pow conserves normalizedness *}
+text \<open>pow conserves normalizedness\<close>
 lemma pow_cn: "isnorm P \<Longrightarrow> isnorm (pow n P)"
 proof (induct n arbitrary: P rule: less_induct)
   case (less k)