Re: [isabelle] What are the Rules and Axioms of Isabelle/HOL Exactly?



On Thu, 14 Jan 2010, Matthew Wampler-Doty wrote:

Well, I am personally interested in the axioms and rules of
Isabelle/Pure, since I would like to know how they compare to
HOL-Light, the other system which I am familiar.

See also sections 2.3 and 2.4 in http://isabelle.in.tum.de/documentation.html

This disentangles a bit the primitive vs. derived rules that also happen to be in our inference kernel.


	Makarius






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.