equal
deleted
inserted
replaced
14 |
14 |
15 subsubsection{*Congruence Rules*} |
15 subsubsection{*Congruence Rules*} |
16 |
16 |
17 text{*\label{sec:simp-cong} |
17 text{*\label{sec:simp-cong} |
18 While simplifying the conclusion $Q$ |
18 While simplifying the conclusion $Q$ |
19 of $P \Imp Q$, it is legal use the assumption $P$. |
19 of $P \Imp Q$, it is legal to use the assumption $P$. |
20 For $\Imp$ this policy is hardwired, but |
20 For $\Imp$ this policy is hardwired, but |
21 contextual information can also be made available for other |
21 contextual information can also be made available for other |
22 operators. For example, @{prop"xs = [] --> xs@xs = xs"} simplifies to @{term |
22 operators. For example, @{prop"xs = [] --> xs@xs = xs"} simplifies to @{term |
23 True} because we may use @{prop"xs = []"} when simplifying @{prop"xs@xs = |
23 True} because we may use @{prop"xs = []"} when simplifying @{prop"xs@xs = |
24 xs"}. The generation of contextual information during simplification is |
24 xs"}. The generation of contextual information during simplification is |