Just to be clear, Tactician (only for HOL Light at the moment) goes between
the three styles:
- g and e
- prove with THEN/THENL/etc
- Flyspeck's 'prove_by_refinement', which is a hybrid of the above two
Mark.
on 18/11/15 8:54 AM, Ramana Kumar wrote:
> I usually use ">>" instead of literally
I usually use ">>" instead of literally "THEN". Arguably that's still too
much "shift".
Yes I think you're right about tactician - it's for going back and forth
between those styles.
On 18 November 2015 at 08:41, Freek Wiedijk wrote:
> Hi Ramana,
>
> >Apparently Coq somewhat recently gained the
Hi Ramana,
>Apparently Coq somewhat recently gained the ability to be explicit about
>proof structure:
>http://poleiro.info/posts/2013-06-27-structuring-proofs-with-bullets.html
>(Of course that comes naturally when using tacticals like THEN, THEN1, etc.)
Not _very_ recently. It was introduced i
Apparently Coq somewhat recently gained the ability to be explicit about
proof structure:
http://poleiro.info/posts/2013-06-27-structuring-proofs-with-bullets.html
(Of course that comes naturally when using tacticals like THEN, THEN1, etc.)
--
