--- a/src/Doc/Tutorial/Types/Overloading.thy Thu Jan 11 13:48:17 2018 +0100
+++ b/src/Doc/Tutorial/Types/Overloading.thy Fri Jan 12 14:08:53 2018 +0100
@@ -2,76 +2,76 @@
hide_class (open) plus (*>*)
-text {* Type classes allow \emph{overloading}; thus a constant may
-have multiple definitions at non-overlapping types. *}
+text \<open>Type classes allow \emph{overloading}; thus a constant may
+have multiple definitions at non-overlapping types.\<close>
-subsubsection {* Overloading *}
+subsubsection \<open>Overloading\<close>
-text {* We can introduce a binary infix addition operator @{text "\<oplus>"}
-for arbitrary types by means of a type class: *}
+text \<open>We can introduce a binary infix addition operator @{text "\<oplus>"}
+for arbitrary types by means of a type class:\<close>
class plus =
fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<oplus>" 70)
-text {* \noindent This introduces a new class @{class [source] plus},
+text \<open>\noindent This introduces a new class @{class [source] plus},
along with a constant @{const [source] plus} with nice infix syntax.
@{const [source] plus} is also named \emph{class operation}. The type
of @{const [source] plus} carries a class constraint @{typ [source] "'a
:: plus"} on its type variable, meaning that only types of class
@{class [source] plus} can be instantiated for @{typ [source] "'a"}.
To breathe life into @{class [source] plus} we need to declare a type
-to be an \bfindex{instance} of @{class [source] plus}: *}
+to be an \bfindex{instance} of @{class [source] plus}:\<close>
instantiation nat :: plus
begin
-text {* \noindent Command \isacommand{instantiation} opens a local
+text \<open>\noindent Command \isacommand{instantiation} opens a local
theory context. Here we can now instantiate @{const [source] plus} on
-@{typ nat}: *}
+@{typ nat}:\<close>
primrec plus_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
"(0::nat) \<oplus> n = n"
| "Suc m \<oplus> n = Suc (m \<oplus> n)"
-text {* \noindent Note that the name @{const [source] plus} carries a
+text \<open>\noindent Note that the name @{const [source] plus} carries a
suffix @{text "_nat"}; by default, the local name of a class operation
@{text f} to be instantiated on type constructor @{text \<kappa>} is mangled
as @{text f_\<kappa>}. In case of uncertainty, these names may be inspected
using the @{command "print_context"} command.
Although class @{class [source] plus} has no axioms, the instantiation must be
-formally concluded by a (trivial) instantiation proof ``..'': *}
+formally concluded by a (trivial) instantiation proof ``..'':\<close>
instance ..
-text {* \noindent More interesting \isacommand{instance} proofs will
+text \<open>\noindent More interesting \isacommand{instance} proofs will
arise below.
-The instantiation is finished by an explicit *}
+The instantiation is finished by an explicit\<close>
end
-text {* \noindent From now on, terms like @{term "Suc (m \<oplus> 2)"} are
-legal. *}
+text \<open>\noindent From now on, terms like @{term "Suc (m \<oplus> 2)"} are
+legal.\<close>
instantiation prod :: (plus, plus) plus
begin
-text {* \noindent Here we instantiate the product type @{type prod} to
+text \<open>\noindent Here we instantiate the product type @{type prod} to
class @{class [source] plus}, given that its type arguments are of
-class @{class [source] plus}: *}
+class @{class [source] plus}:\<close>
fun plus_prod :: "'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b" where
"(x, y) \<oplus> (w, z) = (x \<oplus> w, y \<oplus> z)"
-text {* \noindent Obviously, overloaded specifications may include
-recursion over the syntactic structure of types. *}
+text \<open>\noindent Obviously, overloaded specifications may include
+recursion over the syntactic structure of types.\<close>
instance ..
end
-text {* \noindent This way we have encoded the canonical lifting of
-binary operations to products by means of type classes. *}
+text \<open>\noindent This way we have encoded the canonical lifting of
+binary operations to products by means of type classes.\<close>
(*<*)end(*>*)