equal
deleted
inserted
replaced
110 Simplification terminates for these proofs because the condition of the \isa{if} simplifies to \isa{True} or \isa{False}. |
110 Simplification terminates for these proofs because the condition of the \isa{if} simplifies to \isa{True} or \isa{False}. |
111 Now we can disable the original simplification rule:% |
111 Now we can disable the original simplification rule:% |
112 \end{isamarkuptext}% |
112 \end{isamarkuptext}% |
113 \isamarkuptrue% |
113 \isamarkuptrue% |
114 \isacommand{declare}\ gcd{\isachardot}simps\ {\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline |
114 \isacommand{declare}\ gcd{\isachardot}simps\ {\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline |
|
115 \isanewline |
115 \isamarkupfalse% |
116 \isamarkupfalse% |
116 \isanewline |
|
117 \isamarkupfalse% |
117 \isamarkupfalse% |
118 \end{isabellebody}% |
118 \end{isabellebody}% |
119 %%% Local Variables: |
119 %%% Local Variables: |
120 %%% mode: latex |
120 %%% mode: latex |
121 %%% TeX-master: "root" |
121 %%% TeX-master: "root" |