| changeset 30270 | 61811c9224a6 |
| parent 29774 | 829e52cd135d |
| child 30272 | 2d612824e642 |
| 30236:e70dae49dc57 | 30270:61811c9224a6 |
|---|---|
903 compared to @{text "RS"}, the rule argument order is swapped: @{text |
903 compared to @{text "RS"}, the rule argument order is swapped: @{text |
904 "rule\<^sub>1 RS rule\<^sub>2 = rule\<^sub>2 OF [rule\<^sub>1]"}. |
904 "rule\<^sub>1 RS rule\<^sub>2 = rule\<^sub>2 OF [rule\<^sub>1]"}. |
905 |
905 |
906 \end{description} |
906 \end{description} |
907 *} |
907 *} |
908 |
908 |
909 end |
909 end |