equal
deleted
inserted
replaced
1 \begin{isabelle}% |
1 % |
|
2 \begin{isabellebody}% |
2 % |
3 % |
3 \begin{isamarkuptext}% |
4 \begin{isamarkuptext}% |
4 When a function is defined via \isacommand{recdef}, Isabelle tries to prove |
5 When a function is defined via \isacommand{recdef}, Isabelle tries to prove |
5 its termination with the help of the user-supplied measure. All of the above |
6 its termination with the help of the user-supplied measure. All of the above |
6 examples are simple enough that Isabelle can prove automatically that the |
7 examples are simple enough that Isabelle can prove automatically that the |
84 \begin{isamarkuptext}% |
85 \begin{isamarkuptext}% |
85 \noindent |
86 \noindent |
86 For details see the manual~\cite{isabelle-HOL} and the examples in the |
87 For details see the manual~\cite{isabelle-HOL} and the examples in the |
87 library.% |
88 library.% |
88 \end{isamarkuptext}% |
89 \end{isamarkuptext}% |
89 \end{isabelle}% |
90 \end{isabellebody}% |
90 %%% Local Variables: |
91 %%% Local Variables: |
91 %%% mode: latex |
92 %%% mode: latex |
92 %%% TeX-master: "root" |
93 %%% TeX-master: "root" |
93 %%% End: |
94 %%% End: |