equal
deleted
inserted
replaced
1015 \begin{warn} |
1015 \begin{warn} |
1016 Casual readers should skip the rest of this section. We use fixed point |
1016 Casual readers should skip the rest of this section. We use fixed point |
1017 operators only in \S\ref{sec:VMC}. |
1017 operators only in \S\ref{sec:VMC}. |
1018 \end{warn} |
1018 \end{warn} |
1019 |
1019 |
1020 The theory applies only to monotonic functions. Isabelle's |
1020 The theory applies only to monotonic functions.\index{monotone functions|bold} |
1021 definition of monotone is overloaded over all orderings: |
1021 Isabelle's definition of monotone is overloaded over all orderings: |
1022 \begin{isabelle} |
1022 \begin{isabelle} |
1023 mono\ f\ \isasymequiv\ {\isasymforall}A\ B.\ A\ \isasymle\ B\ \isasymlongrightarrow\ f\ A\ \isasymle\ f\ B% |
1023 mono\ f\ \isasymequiv\ {\isasymforall}A\ B.\ A\ \isasymle\ B\ \isasymlongrightarrow\ f\ A\ \isasymle\ f\ B% |
1024 \rulename{mono_def} |
1024 \rulename{mono_def} |
1025 \end{isabelle} |
1025 \end{isabelle} |
1026 % |
1026 % |