On 19.02.2014 14:41, Bill Richter wrote:
> - if you have existentials or disjunctions in the theorems you want to
> use or in the goal, use MESON_TAC
>
> By putting this after SIMP_TAC, I infer that SIMP_TAC will not handle
> existentials or disjunctions.
Indeed - most of the time.
Let me
Vince, thanks for improving my code! I've implemented Freek's 1-line "by"
proofs, so I can shorten your proof a bit:
let INTERIOR_EQ = theorem `;
∀s. interior s = s ⇔ open s
by simplify interior_DEF OPEN_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN InteriorEq
EQ_SYM_EQ`;;
But why does this work? L
