equal
deleted
inserted
replaced
163 |
163 |
164 txt{*\noindent |
164 txt{*\noindent |
165 We get the following proof state: |
165 We get the following proof state: |
166 @{subgoals[display,indent=0,margin=65]} |
166 @{subgoals[display,indent=0,margin=65]} |
167 After stripping the @{text"\<forall>i"}, the proof continues with a case |
167 After stripping the @{text"\<forall>i"}, the proof continues with a case |
168 distinction on @{term"i"}. The case @{prop"i = 0"} is trivial and we focus on |
168 distinction on @{term"i"}. The case @{prop"i = (0::nat)"} is trivial and we focus on |
169 the other case: |
169 the other case: |
170 *} |
170 *} |
171 |
171 |
172 apply(rule allI) |
172 apply(rule allI) |
173 apply(case_tac i) |
173 apply(case_tac i) |