Back to my other question, there's something about USE_THEN and type
annotations I don't understand. I get the same problem with FIRST_ASSUM. In
Multivariate/topology.ml there's a theorem
let FRONTIER_CLOSURES = prove
(`!s:real^N->bool. frontier s = (closure s) INTER (closure(UNIV DIFF s))`,
Thanks, Vince! I think we haven't quite gotten it right yet, as it's tricky to
talk about intentions. You correctly pointed out there was something wrong
with the way I used REWRITE_TAC[DIST_SYM]. John's proof uses ONCE_REWRITE_TAC
correctly, but he's using DIST_TRIANGLE_ALT, while I tried to
On 17.02.2014 12:49, Bill Richter wrote:
> Vince, this is very interesting:
>
> I would say what is bad coding is not to rely on features you don't
> understand but on features that are actually
> undocumented/unintended. Here, the ordering chosen is indeed
> ingenious to prevent s
Vince, this is very interesting:
I would say what is bad coding is not to rely on features you don't
understand but on features that are actually
undocumented/unintended. Here, the ordering chosen is indeed
ingenious to prevent some often-met looping situations. However,
as John p
Thanks for correcting me, Adnan and Vince, POP_ASSUM does indeed remove the
assumption:
# help "POP_ASSUM";;
---
When applied to a theorem-tactic and a goal, POP_ASSUM applies
the theorem-tactic to the first element of the assumpti
