equal
deleted
inserted
replaced
1 \begin{isabelle}% |
1 % |
|
2 \begin{isabellebody}% |
2 % |
3 % |
3 \begin{isamarkuptext}% |
4 \begin{isamarkuptext}% |
4 So far all examples of rewrite rules were equations. The simplifier also |
5 So far all examples of rewrite rules were equations. The simplifier also |
5 accepts \emph{conditional} equations, for example% |
6 accepts \emph{conditional} equations, for example% |
6 \end{isamarkuptext}% |
7 \end{isamarkuptext}% |
21 can simplify \isa{hd(rev~xs)~\#~tl(rev~xs)} to \isa{rev xs} |
22 can simplify \isa{hd(rev~xs)~\#~tl(rev~xs)} to \isa{rev xs} |
22 because the corresponding precondition \isa{rev xs \isasymnoteq\ []} |
23 because the corresponding precondition \isa{rev xs \isasymnoteq\ []} |
23 simplifies to \isa{xs \isasymnoteq\ []}, which is exactly the local |
24 simplifies to \isa{xs \isasymnoteq\ []}, which is exactly the local |
24 assumption of the subgoal.% |
25 assumption of the subgoal.% |
25 \end{isamarkuptext}% |
26 \end{isamarkuptext}% |
26 \end{isabelle}% |
27 \end{isabellebody}% |
27 %%% Local Variables: |
28 %%% Local Variables: |
28 %%% mode: latex |
29 %%% mode: latex |
29 %%% TeX-master: "root" |
30 %%% TeX-master: "root" |
30 %%% End: |
31 %%% End: |