Hi Joe,
On 04/11/2015 18:07, Joe Leslie-Hurd wrote: > I was thinking of a lightweight HOL Light mode that highlighted quoted > terms/tacticals/etc and knew about indentation of tactic proofs, > rather than extending an OCaml mode that has a lot of features that > don't really apply to HOL Light tactic proofs. That would be very helpful. Tuareg mode is far from ideal for HOL Light (especially when handling backquoted terms and tacticals). > I have never used tactician, and would be curious how these simple > macros compare. > > The macros nicely automate what I (at least) do very often manually. Tactician is more general and gives you a full breakdown of the packaged proof in interactive steps (and vice-versa), at the cost of having to reconstruct core HOL Light data structures. Of course Mark would be much better at explaining more details. One advantage that I can think of is when you wish to go through the proof of one particular subgoal. This may be confusing if you are executing packaged proof steps (e.g. if other subgoals are proven simultaneously). Regards, Petros -- Petros Papapanagiotou, Ph.D. CISA, School of Informatics The University of Edinburgh Email: p...@ed.ac.uk --- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
