equal
deleted
inserted
replaced
88 txt{* |
88 txt{* |
89 @{subgoals[display,indent=0,margin=65]} |
89 @{subgoals[display,indent=0,margin=65]} |
90 |
90 |
91 \noindent |
91 \noindent |
92 The inclusion remains to be proved. After unfolding some definitions, |
92 The inclusion remains to be proved. After unfolding some definitions, |
93 we are left with simple arithmetic: |
93 we are left with simple arithmetic that is dispatched automatically. |
94 *} |
94 *} |
95 |
95 |
96 apply (clarify, simp add: measure_def inv_image_def) |
96 by (clarify, simp add: measure_def inv_image_def) |
97 |
|
98 txt{* |
|
99 @{subgoals[display,indent=0,margin=65]} |
|
100 |
|
101 \noindent |
|
102 And that is dispatched automatically: |
|
103 *} |
|
104 |
|
105 by arith |
|
106 |
97 |
107 text{*\noindent |
98 text{*\noindent |
108 |
99 |
109 Armed with this lemma, we use the \attrdx{recdef_wf} attribute to attach a |
100 Armed with this lemma, we use the \attrdx{recdef_wf} attribute to attach a |
110 crucial hint\cmmdx{hints} to our definition: |
101 crucial hint\cmmdx{hints} to our definition: |