Folks,
What is wrong with the Euclid example?
Pg 30 of the tutorial?
The `0` won't parse and I get
> e (qexists_tac `0`);
OK..
Exception raised at Tactical.Q_TAC:
No parse for quotation
Exception-
HOL_ERR
{message = "No parse for quotation", origin_function = "Q_TAC",
origin_structure = "Tactical"} raised
Thanks, Brian
--
Take em to church Billy (Payne). - Paul Barrere
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
