equal
deleted
inserted
replaced
57 Table~\ref{tab:overloading} in the appendix shows the most important overloaded |
57 Table~\ref{tab:overloading} in the appendix shows the most important overloaded |
58 operations. |
58 operations. |
59 \end{warn} |
59 \end{warn} |
60 |
60 |
61 Simple arithmetic goals are proved automatically by both @{term auto} and the |
61 Simple arithmetic goals are proved automatically by both @{term auto} and the |
62 simplification methods introduced in \S\ref{sec:Simplification}. For |
62 simplification method introduced in \S\ref{sec:Simplification}. For |
63 example, |
63 example, |
64 *} |
64 *} |
65 |
65 |
66 lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n" |
66 lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n" |
67 (*<*)by(auto)(*>*) |
67 (*<*)by(auto)(*>*) |