src/Doc/Tutorial/Recdef/examples.thy

--- a/src/Doc/Tutorial/Recdef/examples.thy	Thu Jan 11 13:48:17 2018 +0100
+++ b/src/Doc/Tutorial/Recdef/examples.thy	Fri Jan 12 14:08:53 2018 +0100
@@ -2,9 +2,9 @@
 theory examples imports Main begin
 (*>*)
 
-text{*
+text\<open>
 Here is a simple example, the \rmindex{Fibonacci function}:
-*}
+\<close>
 
 consts fib :: "nat \<Rightarrow> nat"
 recdef fib "measure(\<lambda>n. n)"
@@ -12,7 +12,7 @@
   "fib (Suc 0) = 1"
   "fib (Suc(Suc x)) = fib x + fib (Suc x)"
 
-text{*\noindent
+text\<open>\noindent
 \index{measure functions}%
 The definition of @{term"fib"} is accompanied by a \textbf{measure function}
 @{term"%n. n"} which maps the argument of @{term"fib"} to a
@@ -25,7 +25,7 @@
 
 Slightly more interesting is the insertion of a fixed element
 between any two elements of a list:
-*}
+\<close>
 
 consts sep :: "'a \<times> 'a list \<Rightarrow> 'a list"
 recdef sep "measure (\<lambda>(a,xs). length xs)"
@@ -33,7 +33,7 @@
   "sep(a, [x])    = [x]"
   "sep(a, x#y#zs) = x # a # sep(a,y#zs)"
 
-text{*\noindent
+text\<open>\noindent
 This time the measure is the length of the list, which decreases with the
 recursive call; the first component of the argument tuple is irrelevant.
 The details of tupled $\lambda$-abstractions @{text"\<lambda>(x\<^sub>1,\<dots>,x\<^sub>n)"} are
@@ -41,24 +41,24 @@
 
 Pattern matching\index{pattern matching!and \isacommand{recdef}}
 need not be exhaustive:
-*}
+\<close>
 
 consts last :: "'a list \<Rightarrow> 'a"
 recdef last "measure (\<lambda>xs. length xs)"
   "last [x]      = x"
   "last (x#y#zs) = last (y#zs)"
 
-text{*
+text\<open>
 Overlapping patterns are disambiguated by taking the order of equations into
 account, just as in functional programming:
-*}
+\<close>
 
 consts sep1 :: "'a \<times> 'a list \<Rightarrow> 'a list"
 recdef sep1 "measure (\<lambda>(a,xs). length xs)"
   "sep1(a, x#y#zs) = x # a # sep1(a,y#zs)"
   "sep1(a, xs)     = xs"
 
-text{*\noindent
+text\<open>\noindent
 To guarantee that the second equation can only be applied if the first
 one does not match, Isabelle internally replaces the second equation
 by the two possibilities that are left: @{prop"sep1(a,[]) = []"} and
@@ -73,17 +73,17 @@
   argument is relevant for termination, you can also rearrange the order of
   arguments as in the following definition:
 \end{warn}
-*}
+\<close>
 consts sep2 :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
 recdef sep2 "measure length"
   "sep2 (x#y#zs) = (\<lambda>a. x # a # sep2 (y#zs) a)"
   "sep2 xs       = (\<lambda>a. xs)"
 
-text{*
+text\<open>
 Because of its pattern-matching syntax, \isacommand{recdef} is also useful
 for the definition of non-recursive functions, where the termination measure
 degenerates to the empty set @{term"{}"}:
-*}
+\<close>
 
 consts swap12 :: "'a list \<Rightarrow> 'a list"
 recdef swap12 "{}"