more xsymbols
authorhaftmann
Fri Aug 27 14:22:15 2010 +0200 (2010-08-27)
changeset 38811c3511b112595
parent 38810 361119ea62ee
child 38812 e527a34bf69d
more xsymbols
doc-src/Codegen/Thy/Inductive_Predicate.thy
     1.1 --- a/doc-src/Codegen/Thy/Inductive_Predicate.thy	Fri Aug 27 13:55:23 2010 +0200
     1.2 +++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy	Fri Aug 27 14:22:15 2010 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  inductive %invisible append where
     1.6    "append [] ys ys"
     1.7 -| "append xs ys zs ==> append (x # xs) ys (x # zs)"
     1.8 +| "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
     1.9  
    1.10  lemma %invisible append: "append xs ys zs = (xs @ ys = zs)"
    1.11    by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros)
    1.12 @@ -95,9 +95,9 @@
    1.13    "append_i_i_o"}).  You can specify your own names as follows:
    1.14  *}
    1.15  
    1.16 -code_pred %quote (modes: i => i => o => bool as concat,
    1.17 -  o => o => i => bool as split,
    1.18 -  i => o => i => bool as suffix) append .
    1.19 +code_pred %quote (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as concat,
    1.20 +  o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as split,
    1.21 +  i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix) append .
    1.22  
    1.23  subsection {* Alternative introduction rules *}
    1.24  
    1.25 @@ -220,8 +220,8 @@
    1.26    "values"} and the number of elements.
    1.27  *}
    1.28  
    1.29 -values %quote [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
    1.30 -values %quote [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
    1.31 +values %quote [mode: i \<Rightarrow> o \<Rightarrow> bool] 20 "{n. tranclp succ 10 n}"
    1.32 +values %quote [mode: o \<Rightarrow> i \<Rightarrow> bool] 10 "{n. tranclp succ n 10}"
    1.33  
    1.34  
    1.35  subsection {* Embedding into functional code within Isabelle/HOL *}