equal
deleted
inserted
replaced
58 case b |
58 case b |
59 then show ?thesis <proof> |
59 then show ?thesis <proof> |
60 next |
60 next |
61 case c |
61 case c |
62 then show ?thesis <proof> |
62 then show ?thesis <proof> |
|
63 qed |
|
64 |
|
65 * Nesting of Isar goal structure has been clarified: the context after |
|
66 the initial backwards refinement is retained for the whole proof, within |
|
67 all its context sections (as indicated via 'next'). This is e.g. |
|
68 relevant for 'using', 'including', 'supply': |
|
69 |
|
70 have "A \<and> A" if a: A for A |
|
71 supply [simp] = a |
|
72 proof |
|
73 show A by simp |
|
74 next |
|
75 show A by simp |
63 qed |
76 qed |
64 |
77 |
65 |
78 |
66 *** Pure *** |
79 *** Pure *** |
67 |
80 |