--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Thu May 26 17:51:22 2016 +0200
@@ -108,7 +108,7 @@
end
-text{* The integers form a @{text comm_ring_1}*}
+text\<open>The integers form a \<open>comm_ring_1\<close>\<close>
instance int :: comm_ring_1
proof
@@ -235,7 +235,7 @@
using a
by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)
-text{*The integers form an ordered integral domain*}
+text\<open>The integers form an ordered integral domain\<close>
instance int :: linordered_idom
proof
@@ -276,7 +276,7 @@
by (descending) (auto intro: int_induct2)
-text {* Magnitide of an Integer, as a Natural Number: @{term nat} *}
+text \<open>Magnitide of an Integer, as a Natural Number: @{term nat}\<close>
definition
"int_to_nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"