equal
deleted
inserted
replaced
70 |
70 |
71 Before we start on any proofs about \isa{update} we tell the simplifier to |
71 Before we start on any proofs about \isa{update} we tell the simplifier to |
72 expand all \isa{let}s and to split all \isa{case}-constructs over |
72 expand all \isa{let}s and to split all \isa{case}-constructs over |
73 options:% |
73 options:% |
74 \end{isamarkuptext}% |
74 \end{isamarkuptext}% |
75 \isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\isanewline |
75 \isacommand{declare}\ Let{\isacharunderscore}def{\isacharbrackleft}simp{\isacharbrackright}\ option{\isachardot}split{\isacharbrackleft}split{\isacharbrackright}% |
76 \isacommand{lemmas}\ {\isacharbrackleft}split{\isacharbrackright}\ {\isacharequal}\ option{\isachardot}split% |
|
77 \begin{isamarkuptext}% |
76 \begin{isamarkuptext}% |
78 \noindent |
77 \noindent |
79 The reason becomes clear when looking (probably after a failed proof |
78 The reason becomes clear when looking (probably after a failed proof |
80 attempt) at the body of \isa{update}: it contains both |
79 attempt) at the body of \isa{update}: it contains both |
81 \isa{let} and a case distinction over type \isa{option}. |
80 \isa{let} and a case distinction over type \isa{option}. |