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