Thanks, Petros! I hate to be an ingrate, but could you port one of my longer proofs to IsabelleLight? It might help if you read section 10.1, The bug puzzle, of the HOL Light tutorial, or hol_light/Examples/inverse_bug_puzzle_tac.ml. Thanks for telling me about cases: I'll change the name. What I mainly want is to replicate in tactics proofs an accomplishment of Freek's in miz3.ml: maintaining an environment so that variables don't have to be repeatedly typed. Are you trying to do that in IsabelleLight? Freek did this, by changing the parser, and Vince has been advising me on how to do this myself. Are you planning to change the parser as well, or does IsabelleLight have a different idea for the environment?
Also, you lose some of the labelling functionality that you have from the recently added tactics (HYP, INTRO_TAC etc). It would take a bit of work to build this into Isabelle Light which I'm hoping to find some time to do. Excellent! I apologize for not having read your code yet. I just learned about another formalization of Tarski's axiomatic geometry, one using the proof assistant otter, which I know little about: http://www.michaelbeeson.com/research/FormalTarski/index.php Michael Beeson and Julien Narboux both got quite a bit farther than I did: http://www.math.northwestern.edu/~richter/TarskiAxiomGeometry.ml Does anyone know about otter, or how far Julien is on his Tarski project? -- Best, Bill ------------------------------------------------------------------------------ Precog is a next-generation analytics platform capable of advanced analytics on semi-structured data. The platform includes APIs for building apps and a phenomenal toolset for data science. Developers can use our toolset for easy data analysis & visualization. Get a free account! http://www2.precog.com/precogplatform/slashdotnewsletter _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
