Hello, You might find Mark Adams's Tactician helpful: http://www.proof-technologies.com/tactician/index.html
It can break down "packaged" proofs to g() and e() statements (among other things). I am not aware of any other alternatives. Also, unless I misunderstood, you can use b() to undo a proof step in an interactive proof. Hope this helps. Regards, Petros On 13/03/2015 00:07, Mario Carneiro wrote: > Hello all, > > What is the usual method for "viewing" a proof stored in HOL Light, if > you wanted to read it like a regular math textbook (assuming you can get > over syntax difficulties)? (Of course it is not really feasible to look > at the code in isolation, because you can't see the formulas.) The > method I have been using so far is to copy the tactics one at a time > into a HOL session using g() and e(), but it's very tedious and > time-consuming, and it is also difficult to undo if you make a copying > mistake during the process. (I should note that I am still a relative > newbie to using HOL Light and this is essentially the only thing I have > tried to do with it - I have yet to write an actual proof of my own in > HOL Light.) > > I feel like this is a common enough goal that there should be some > program to do what I am doing and log the output. Better yet, if there > was a website or downloadable collection of these proofs processed into > a form that did not require interactivity in the OCaml session, this > would make it much easier for mathematicians who do not necessarily want > to write proofs but want to examine the many existing HOL Light proofs > in order to understand them (like me). Does such a thing exist? > > Mario Carneiro > > > ------------------------------------------------------------------------------ > Dive into the World of Parallel Programming The Go Parallel Website, sponsored > by Intel and developed in partnership with Slashdot Media, is your hub for all > things parallel software development, from weekly thought leadership blogs to > news, videos, case studies, tutorials and more. Take a look and join the > conversation now. http://goparallel.sourceforge.net/ > > > > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > -- 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. ------------------------------------------------------------------------------ Dive into the World of Parallel Programming The Go Parallel Website, sponsored by Intel and developed in partnership with Slashdot Media, is your hub for all things parallel software development, from weekly thought leadership blogs to news, videos, case studies, tutorials and more. Take a look and join the conversation now. http://goparallel.sourceforge.net/ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info