# HG changeset patch
# User wenzelm
# Date 1445440898 -7200
# Node ID 32a20d7b3ee451ef2596b9026ad6b5e9b5d0f9c5
# Parent  8b5559c2647cd897cda651388d66617724cc3f2d
tuned document;

diff -r 8b5559c2647c -r 32a20d7b3ee4 src/Doc/Codegen/Inductive_Predicate.thy
--- a/src/Doc/Codegen/Inductive_Predicate.thy	Wed Oct 21 16:54:15 2015 +0200
+++ b/src/Doc/Codegen/Inductive_Predicate.thy	Wed Oct 21 17:21:38 2015 +0200
@@ -225,7 +225,7 @@
   "values"} and the number of elements.
 \<close>
 
-values %quote [mode: i \<Rightarrow> o \<Rightarrow> bool] 1 "{n. tranclp succ 10 n}" (*FIMXE does not terminate for n\<ge>1*)
+values %quote [mode: i \<Rightarrow> o \<Rightarrow> bool] 1 "{n. tranclp succ 10 n}" (*FIXME does not terminate for n\<ge>1*)
 values %quote [mode: o \<Rightarrow> i \<Rightarrow> bool] 1 "{n. tranclp succ n 10}"
 
 
@@ -237,25 +237,22 @@
 
   \begin{itemize}
 
-    \item You want to use the first-order predicate with the mode
-      where all arguments are input. Then you can use the predicate directly, e.g.
+  \item You want to use the first-order predicate with the mode
+    where all arguments are input. Then you can use the predicate directly, e.g.
 
-      \begin{quote}
-        @{text "valid_suffix ys zs = "} \\
-        @{text "(if append [Suc 0, 2] ys zs then Some ys else None)"}
-      \end{quote}
+    @{text [display]
+\<open>valid_suffix ys zs =
+  (if append [Suc 0, 2] ys zs then Some ys else None)\<close>}
 
-    \item If you know that the execution returns only one value (it is
-      deterministic), then you can use the combinator @{term
-      "Predicate.the"}, e.g., a functional concatenation of lists is
-      defined with
+  \item If you know that the execution returns only one value (it is
+    deterministic), then you can use the combinator @{term
+    "Predicate.the"}, e.g., a functional concatenation of lists is
+    defined with
 
-      \begin{quote}
-        @{term "functional_concat xs ys = Predicate.the (append_i_i_o xs ys)"}
-      \end{quote}
+    @{term [display] "functional_concat xs ys = Predicate.the (append_i_i_o xs ys)"}
 
-      Note that if the evaluation does not return a unique value, it
-      raises a run-time error @{term "not_unique"}.
+    Note that if the evaluation does not return a unique value, it
+    raises a run-time error @{term "not_unique"}.
 
   \end{itemize}
 \<close>