equal
deleted
inserted
replaced
58 it happend \emph{completely} outside the logic. |
58 it happend \emph{completely} outside the logic. |
59 \end{warn} |
59 \end{warn} |
60 *} |
60 *} |
61 |
61 |
62 text {* |
62 text {* |
63 Consider the following function and its corresponding |
63 \noindent Consider the following function and its corresponding |
64 SML code: |
64 SML code: |
65 *} |
65 *} |
66 |
66 |
67 primrec %quoteme in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where |
67 primrec %quoteme in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where |
68 "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l" |
68 "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l" |