--- a/src/Doc/Tutorial/Types/Pairs.thy Sat Jan 05 17:00:43 2019 +0100
+++ b/src/Doc/Tutorial/Types/Pairs.thy Sat Jan 05 17:24:33 2019 +0100
@@ -4,8 +4,8 @@
text\<open>\label{sec:products}
Ordered pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal
-repertoire of operations: pairing and the two projections @{term fst} and
-@{term snd}. In any non-trivial application of pairs you will find that this
+repertoire of operations: pairing and the two projections \<^term>\<open>fst\<close> and
+\<^term>\<open>snd\<close>. In any non-trivial application of pairs you will find that this
quickly leads to unreadable nests of projections. This
section introduces syntactic sugar to overcome this
problem: pattern matching with tuples.
@@ -20,11 +20,11 @@
and they can be nested. Here are
some typical examples:
\begin{quote}
-@{term"let (x,y) = f z in (y,x)"}\\
-@{term"case xs of [] => (0::nat) | (x,y)#zs => x+y"}\\
+\<^term>\<open>let (x,y) = f z in (y,x)\<close>\\
+\<^term>\<open>case xs of [] => (0::nat) | (x,y)#zs => x+y\<close>\\
\<open>\<forall>(x,y)\<in>A. x=y\<close>\\
\<open>{(x,y,z). x=z}\<close>\\
-@{term"\<Union>(x,y)\<in>A. {x+y}"}
+\<^term>\<open>\<Union>(x,y)\<in>A. {x+y}\<close>
\end{quote}
The intuitive meanings of these expressions should be obvious.
Unfortunately, we need to know in more detail what the notation really stands
@@ -32,11 +32,11 @@
over pairs and tuples is merely a convenient shorthand for a more complex
internal representation. Thus the internal and external form of a term may
differ, which can affect proofs. If you want to avoid this complication,
-stick to @{term fst} and @{term snd} and write @{term"%p. fst p + snd p"}
+stick to \<^term>\<open>fst\<close> and \<^term>\<open>snd\<close> and write \<^term>\<open>%p. fst p + snd p\<close>
instead of \<open>\<lambda>(x,y). x+y\<close>. These terms are distinct even though they
denote the same function.
-Internally, @{term"%(x,y). t"} becomes \<open>case_prod (\<lambda>x y. t)\<close>, where
+Internally, \<^term>\<open>%(x,y). t\<close> becomes \<open>case_prod (\<lambda>x y. t)\<close>, where
\cdx{split} is the uncurrying function of type \<open>('a \<Rightarrow> 'b
\<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c\<close> defined as
\begin{center}
@@ -51,7 +51,7 @@
subsection\<open>Theorem Proving\<close>
text\<open>
-The most obvious approach is the brute force expansion of @{term split}:
+The most obvious approach is the brute force expansion of \<^term>\<open>split\<close>:
\<close>
lemma "(\<lambda>(x,y).x) p = fst p"
@@ -60,19 +60,18 @@
text\<open>\noindent
This works well if rewriting with @{thm[source]split_def} finishes the
proof, as it does above. But if it does not, you end up with exactly what
-we are trying to avoid: nests of @{term fst} and @{term snd}. Thus this
+we are trying to avoid: nests of \<^term>\<open>fst\<close> and \<^term>\<open>snd\<close>. Thus this
approach is neither elegant nor very practical in large examples, although it
can be effective in small ones.
If we consider why this lemma presents a problem,
-we realize that we need to replace variable~@{term
-p} by some pair @{term"(a,b)"}. Then both sides of the
-equation would simplify to @{term a} by the simplification rules
+we realize that we need to replace variable~\<^term>\<open>p\<close> by some pair \<^term>\<open>(a,b)\<close>. Then both sides of the
+equation would simplify to \<^term>\<open>a\<close> by the simplification rules
@{thm split_conv[no_vars]} and @{thm fst_conv[no_vars]}.
To reason about tuple patterns requires some way of
converting a variable of product type into a pair.
-In case of a subterm of the form @{term"case_prod f p"} this is easy: the split
-rule @{thm[source]prod.split} replaces @{term p} by a pair:%
+In case of a subterm of the form \<^term>\<open>case_prod f p\<close> this is easy: the split
+rule @{thm[source]prod.split} replaces \<^term>\<open>p\<close> by a pair:%
\index{*split (method)}
\<close>
@@ -110,7 +109,7 @@
@{subgoals[display,indent=0]}
Again, simplification produces a term suitable for @{thm[source]prod.split}
as above. If you are worried about the strange form of the premise:
-\<open>case_prod (=)\<close> is short for @{term"\<lambda>(x,y). x=y"}.
+\<open>case_prod (=)\<close> is short for \<^term>\<open>\<lambda>(x,y). x=y\<close>.
The same proof procedure works for
\<close>
@@ -119,9 +118,9 @@
txt\<open>\noindent
except that we now have to use @{thm[source]prod.split_asm}, because
-@{term split} occurs in the assumptions.
+\<^term>\<open>split\<close> occurs in the assumptions.
-However, splitting @{term split} is not always a solution, as no @{term split}
+However, splitting \<^term>\<open>split\<close> is not always a solution, as no \<^term>\<open>split\<close>
may be present in the goal. Consider the following function:
\<close>
@@ -137,8 +136,8 @@
txt\<open>\noindent
simplification will do nothing, because the defining equation for
-@{const[source] swap} expects a pair. Again, we need to turn @{term p}
-into a pair first, but this time there is no @{term split} in sight.
+@{const[source] swap} expects a pair. Again, we need to turn \<^term>\<open>p\<close>
+into a pair first, but this time there is no \<^term>\<open>split\<close> in sight.
The only thing we can do is to split the term by hand:
\<close>
apply(case_tac p)