# HG changeset patch
# User haftmann
# Date 1282911735 -7200
# Node ID c3511b11259513f88dbbd7a4ef7b6277ace4ec26
# Parent  361119ea62ee007f8a42e3689b845be89d1b0029
more xsymbols

diff -r 361119ea62ee -r c3511b112595 doc-src/Codegen/Thy/Inductive_Predicate.thy
--- a/doc-src/Codegen/Thy/Inductive_Predicate.thy	Fri Aug 27 13:55:23 2010 +0200
+++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy	Fri Aug 27 14:22:15 2010 +0200
@@ -7,7 +7,7 @@
 
 inductive %invisible append where
   "append [] ys ys"
-| "append xs ys zs ==> append (x # xs) ys (x # zs)"
+| "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
 
 lemma %invisible append: "append xs ys zs = (xs @ ys = zs)"
   by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros)
@@ -95,9 +95,9 @@
   "append_i_i_o"}).  You can specify your own names as follows:
 *}
 
-code_pred %quote (modes: i => i => o => bool as concat,
-  o => o => i => bool as split,
-  i => o => i => bool as suffix) append .
+code_pred %quote (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as concat,
+  o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as split,
+  i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix) append .
 
 subsection {* Alternative introduction rules *}
 
@@ -220,8 +220,8 @@
   "values"} and the number of elements.
 *}
 
-values %quote [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
-values %quote [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
+values %quote [mode: i \<Rightarrow> o \<Rightarrow> bool] 20 "{n. tranclp succ 10 n}"
+values %quote [mode: o \<Rightarrow> i \<Rightarrow> bool] 10 "{n. tranclp succ n 10}"
 
 
 subsection {* Embedding into functional code within Isabelle/HOL *}