I learned a number of basic facts thinking about Vince and Freek's ideas, and
now I have no "unused variable" warnings in
RichterHilbertAxiomGeometry/readable.ml. I have some questions.
I reworked Freek's code to get eliminate the "unused variable" warning I was
getting with `is_thm':
let
CALL FOR PARTICIPATION
FroCoS 2013
9th International Symposium on Frontiers of Combining Systems
Nancy, France
September 18-20, 2013
http://frocos2013.loria.fr/
CALL FOR PARTICIPATION
Applying Mechanised Reasoning in Economics – Making Reasoners Applicable
for Domain Experts
http://www.cs.bham.ac.uk/research/projects/formare/events/informatik2013/
Tutorial at Informatik 2013 – Computer science adapted to humans,
organization and the environment, 43rd ann
