equal
deleted
inserted
replaced
218 "o \<Rightarrow> o \<Rightarrow> bool"} is chosen. To choose another mode for the argument, |
218 "o \<Rightarrow> o \<Rightarrow> bool"} is chosen. To choose another mode for the argument, |
219 you can declare the mode for the argument between the @{command |
219 you can declare the mode for the argument between the @{command |
220 "values"} and the number of elements. |
220 "values"} and the number of elements. |
221 *} |
221 *} |
222 |
222 |
223 values %quote [mode: i \<Rightarrow> o \<Rightarrow> bool] 20 "{n. tranclp succ 10 n}" |
223 values %quote [mode: i \<Rightarrow> o \<Rightarrow> bool] 1 "{n. tranclp succ 10 n}" (*FIMXE does not terminate for n\<ge>1*) |
224 values %quote [mode: o \<Rightarrow> i \<Rightarrow> bool] 10 "{n. tranclp succ n 10}" |
224 values %quote [mode: o \<Rightarrow> i \<Rightarrow> bool] 1 "{n. tranclp succ n 10}" |
225 |
225 |
226 |
226 |
227 subsection {* Embedding into functional code within Isabelle/HOL *} |
227 subsection {* Embedding into functional code within Isabelle/HOL *} |
228 |
228 |
229 text {* |
229 text {* |