equal
deleted
inserted
replaced
1 \begin{isabelle}% |
1 % |
|
2 \begin{isabellebody}% |
2 % |
3 % |
3 \begin{isamarkuptext}% |
4 \begin{isamarkuptext}% |
4 \noindent |
5 \noindent |
5 The termintion condition is easily proved by induction:% |
6 The termintion condition is easily proved by induction:% |
6 \end{isamarkuptext}% |
7 \end{isamarkuptext}% |
75 Note that \isacommand{recdef} feeds on exactly the same \emph{kind} of |
76 Note that \isacommand{recdef} feeds on exactly the same \emph{kind} of |
76 congruence rules as the simplifier (\S\ref{sec:simp-cong}) but that |
77 congruence rules as the simplifier (\S\ref{sec:simp-cong}) but that |
77 declaring a congruence rule for the simplifier does not make it |
78 declaring a congruence rule for the simplifier does not make it |
78 available to \isacommand{recdef}, and vice versa. This is intentional.% |
79 available to \isacommand{recdef}, and vice versa. This is intentional.% |
79 \end{isamarkuptext}% |
80 \end{isamarkuptext}% |
80 \end{isabelle}% |
81 \end{isabellebody}% |
81 %%% Local Variables: |
82 %%% Local Variables: |
82 %%% mode: latex |
83 %%% mode: latex |
83 %%% TeX-master: "root" |
84 %%% TeX-master: "root" |
84 %%% End: |
85 %%% End: |