equal
deleted
inserted
replaced
105 a\ {\isacharplus}\ b\ {\isacharequal}\ b\ {\isacharplus}\ a% |
105 a\ {\isacharplus}\ b\ {\isacharequal}\ b\ {\isacharplus}\ a% |
106 \end{isabelle} |
106 \end{isabelle} |
107 \rulename{add_commute} |
107 \rulename{add_commute} |
108 |
108 |
109 \begin{isabelle}% |
109 \begin{isabelle}% |
110 a\ {\isacharplus}\ {\isacharparenleft}b\ {\isacharplus}\ c{\isacharparenright}\ {\isacharequal}\ b\ {\isacharplus}\ {\isacharparenleft}a\ {\isacharplus}\ c{\isacharparenright}% |
110 b\ {\isacharplus}\ {\isacharparenleft}a\ {\isacharplus}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharplus}\ {\isacharparenleft}b\ {\isacharplus}\ c{\isacharparenright}% |
111 \end{isabelle} |
111 \end{isabelle} |
112 \rulename{add_left_commute} |
112 \rulename{add_left_commute} |
113 |
113 |
114 these form add_ac; similarly there is mult_ac% |
114 these form add_ac; similarly there is mult_ac% |
115 \end{isamarkuptext}% |
115 \end{isamarkuptext}% |