equal
deleted
inserted
replaced
24 \isamarkuptrue% |
24 \isamarkuptrue% |
25 % |
25 % |
26 \begin{isamarkuptext}% |
26 \begin{isamarkuptext}% |
27 \label{sec:simp-cong} |
27 \label{sec:simp-cong} |
28 While simplifying the conclusion $Q$ |
28 While simplifying the conclusion $Q$ |
29 of $P \Imp Q$, it is legal use the assumption $P$. |
29 of $P \Imp Q$, it is legal to use the assumption $P$. |
30 For $\Imp$ this policy is hardwired, but |
30 For $\Imp$ this policy is hardwired, but |
31 contextual information can also be made available for other |
31 contextual information can also be made available for other |
32 operators. For example, \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ xs\ {\isacharat}\ xs\ {\isacharequal}\ xs} simplifies to \isa{True} because we may use \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} when simplifying \isa{xs\ {\isacharat}\ xs\ {\isacharequal}\ xs}. The generation of contextual information during simplification is |
32 operators. For example, \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ xs\ {\isacharat}\ xs\ {\isacharequal}\ xs} simplifies to \isa{True} because we may use \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} when simplifying \isa{xs\ {\isacharat}\ xs\ {\isacharequal}\ xs}. The generation of contextual information during simplification is |
33 controlled by so-called \bfindex{congruence rules}. This is the one for |
33 controlled by so-called \bfindex{congruence rules}. This is the one for |
34 \isa{{\isasymlongrightarrow}}: |
34 \isa{{\isasymlongrightarrow}}: |