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 <ramana.ku...@cl.cam.ac.uk> wrote: > 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 <fr...@cs.ru.nl> wrote: > >> 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 in 8.4, which is >> from late 2011. And maybe Ssreflect had it long before >> that already? (In my opinion Ssreflect is a much underrated >> proof language, even if it looks like perl.) >> >> Of course in Flyspeck many (most?) proofs are the other >> way around, where there is just a list of tactics that is >> processed like you would successively "e" them interactively. >> I think Mark Adams tactician is exactly about converting >> a THEN-THEN proof to that format? >> >> But I agree that a more structured "bulleted" proof is nicer. >> Even though ergonomically of course having to type THEN >> is monstrous. >> >> Freek >> > > > > ---------------------------------------- > > ---------------------------------------------------------------------------- > -- > > > > ---------------------------------------- > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
