equal
deleted
inserted
replaced
79 Before we start on any proofs about @{term"update"} we tell the simplifier to |
79 Before we start on any proofs about @{term"update"} we tell the simplifier to |
80 expand all @{text"let"}s and to split all @{text"case"}-constructs over |
80 expand all @{text"let"}s and to split all @{text"case"}-constructs over |
81 options: |
81 options: |
82 *}; |
82 *}; |
83 |
83 |
84 lemmas [simp] = Let_def; |
84 declare Let_def[simp] option.split[split] |
85 lemmas [split] = option.split; |
|
86 |
85 |
87 text{*\noindent |
86 text{*\noindent |
88 The reason becomes clear when looking (probably after a failed proof |
87 The reason becomes clear when looking (probably after a failed proof |
89 attempt) at the body of @{term"update"}: it contains both |
88 attempt) at the body of @{term"update"}: it contains both |
90 @{text"let"} and a case distinction over type @{text"option"}. |
89 @{text"let"} and a case distinction over type @{text"option"}. |