equal
deleted
inserted
replaced
267 \isacommand{by}\ arith\isanewline |
267 \isacommand{by}\ arith\isanewline |
268 \isanewline |
268 \isanewline |
269 \isamarkupfalse% |
269 \isamarkupfalse% |
270 \isacommand{lemma}\ {\isachardoublequote}abs\ {\isacharparenleft}{\isadigit{2}}{\isacharasterisk}x{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ abs\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequote}\isanewline |
270 \isacommand{lemma}\ {\isachardoublequote}abs\ {\isacharparenleft}{\isadigit{2}}{\isacharasterisk}x{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ abs\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequote}\isanewline |
271 \isamarkupfalse% |
271 \isamarkupfalse% |
272 \isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ zabs{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% |
272 \isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ abs{\isacharunderscore}if{\isacharparenright}\isamarkupfalse% |
273 % |
273 % |
274 \begin{isamarkuptext}% |
274 \begin{isamarkuptext}% |
275 Induction rules for the Integers |
275 Induction rules for the Integers |
276 |
276 |
277 \begin{isabelle}% |
277 \begin{isabelle}% |