Thanks, Vince! It worked, once I substituted your quotexpander into system.ml and restarted HOL Light with ocaml #use "hol.ml";;
Now I can get to work on your exercise. A few questions: Why didn't my attempt work? Why did I get the error message "Exception: Noparse." from let parse_qproof string = (fst o parse_preterm o lex o explode) string;; `;&1 + 1`;; It doesn't look that different from your fix: else if c = ";" then "parse_qproof \""^(String.escaped s)^"\"" else if c = "'" then "(fst o parse_preterm o lex o explode) \"" I assume my problem involves the doublequotes, which I know I don't understand. But your version is fine, and Indeed, however in my opinion, it is a better long-term solution to modify system.ml Sure, I was just borrowing Freek's parse_qproof line for simplicity right now when I don't know much, and it turned out I knew even less than I thought. since others might benefit from having quotations dedicated to preterms (as it is the case for instance in HOL4). That's very interesting. Can you say more? And what do you think of Petros's interesting IsabelleLight possibilities? Would it be possible, do you think, to maintain an environment which would get rid of repeated type annotation without changing the parser? That is, I was amazed by what Petros did for my consider function, but I don't know how far you can do in that direction. -- 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
