equal
deleted
inserted
replaced
43 This makes simplification much faster and is faithful to the evaluation |
43 This makes simplification much faster and is faithful to the evaluation |
44 strategy in programming languages, which is why this is the default |
44 strategy in programming languages, which is why this is the default |
45 congruence rule for @{text if}. Analogous rules control the evaluation of |
45 congruence rule for @{text if}. Analogous rules control the evaluation of |
46 @{text case} expressions. |
46 @{text case} expressions. |
47 |
47 |
48 You can declare your own congruence rules with the attribute @{text cong}, |
48 You can declare your own congruence rules with the attribute \attrdx{cong}, |
49 either globally, in the usual manner, |
49 either globally, in the usual manner, |
50 \begin{quote} |
50 \begin{quote} |
51 \isacommand{declare} \textit{theorem-name} @{text"[cong]"} |
51 \isacommand{declare} \textit{theorem-name} @{text"[cong]"} |
52 \end{quote} |
52 \end{quote} |
53 or locally in a @{text"simp"} call by adding the modifier |
53 or locally in a @{text"simp"} call by adding the modifier |