src/Doc/Functions/Functions.thy

--- a/src/Doc/Functions/Functions.thy	Fri Nov 14 11:19:14 2014 +0100
+++ b/src/Doc/Functions/Functions.thy	Fri Nov 14 17:07:06 2014 +0100
@@ -100,7 +100,7 @@
 lemma "map f (sep x ys) = sep (f x) (map f ys)"
 apply (induct x ys rule: sep.induct)
 
-txt {*
+text {*
   We get three cases, like in the definition.
 
   @{subgoals [display]}
@@ -213,7 +213,7 @@
 termination sum
 apply (relation "measure (\<lambda>(i,N). N + 1 - i)")
 
-txt {*
+text {*
   The \cmd{termination} command sets up the termination goal for the
   specified function @{text "sum"}. If the function name is omitted, it
   implicitly refers to the last function definition.
@@ -397,13 +397,13 @@
   "even n = (n mod 2 = 0)"
   "odd n = (n mod 2 = 1)"
 
-txt {* 
+text {* 
   We apply simultaneous induction, specifying the induction variable
   for both goals, separated by \cmd{and}:  *}
 
 apply (induct n and n rule: even_odd.induct)
 
-txt {* 
+text {* 
   We get four subgoals, which correspond to the clauses in the
   definition of @{const even} and @{const odd}:
   @{subgoals[display,indent=0]}
@@ -413,7 +413,7 @@
 
 apply simp_all
 
-txt {* 
+text {* 
   @{subgoals[display,indent=0]} 
 
   \noindent These can be handled by Isabelle's arithmetic decision procedures.
@@ -437,7 +437,7 @@
   "True"
 apply (induct n rule: even_odd.induct)
 
-txt {*
+text {*
   \noindent Now the third subgoal is a dead end, since we have no
   useful induction hypothesis available:
 
@@ -585,7 +585,7 @@
 | "And2 F p = F"
 | "And2 X X = X"
 
-txt {*
+text {*
   \noindent Now let's look at the proof obligations generated by a
   function definition. In this case, they are:
 
@@ -603,7 +603,7 @@
 
 apply pat_completeness
 
-txt {*
+text {*
   The remaining subgoals express \emph{pattern compatibility}. We do
   allow that an input value matches multiple patterns, but in this
   case, the result (i.e.~the right hand sides of the equations) must
@@ -636,7 +636,7 @@
 | "fib2 1 = 1"
 | "fib2 (n + 2) = fib2 n + fib2 (Suc n)"
 
-txt {*
+text {*
   This kind of matching is again justified by the proof of pattern
   completeness and compatibility. 
   The proof obligation for pattern completeness states that every natural number is
@@ -807,12 +807,12 @@
 
 lemma findzero_zero: "findzero_dom (f, n) \<Longrightarrow> f (findzero f n) = 0"
 
-txt {* \noindent We apply induction as usual, but using the partial induction
+text {* \noindent We apply induction as usual, but using the partial induction
   rule: *}
 
 apply (induct f n rule: findzero.pinduct)
 
-txt {* \noindent This gives the following subgoals:
+text {* \noindent This gives the following subgoals:
 
   @{subgoals[display,indent=0]}
 
@@ -1041,7 +1041,7 @@
   apply (relation "measure (\<lambda>n. n)")
   apply auto
 
-txt {*
+text {*
   We get stuck with the subgoal
 
   @{subgoals[display]}
@@ -1140,7 +1140,7 @@
 *}
 
 termination proof
-  txt {*
+  text {*
 
   As usual, we have to give a wellfounded relation, such that the
   arguments of the recursive calls get smaller. But what exactly are