equal
deleted
inserted
replaced
262 apply (erule exE) |
262 apply (erule exE) |
263 --{* @{subgoals[display,indent=0,margin=65]} *} |
263 --{* @{subgoals[display,indent=0,margin=65]} *} |
264 apply (erule exE) |
264 apply (erule exE) |
265 --{* @{subgoals[display,indent=0,margin=65]} *} |
265 --{* @{subgoals[display,indent=0,margin=65]} *} |
266 apply (rule_tac x="k*ka" in exI) |
266 apply (rule_tac x="k*ka" in exI) |
|
267 --{* @{subgoals[display,indent=0,margin=65]} *} |
267 apply simp |
268 apply simp |
268 done |
269 done |
269 |
270 |
270 text{* |
271 text{* |
271 Hilbert-epsilon theorems*} |
272 Hilbert-epsilon theorems*} |