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


On Thu, 2010-01-14 at 02:16 +0100, Matthew Wampler-Doty wrote:
> I'm formalizing a completeness theorem for a modal logic my MSc thesis
> in Isabelle/HOL, and I would like to have a section outlining the
> axioms and basic rules Isabelle/HOL (since it's an LCF system after
> all, so there shouldn't be too many of these).  I can't seem to figure
> out how to find these out; they appear to be scattered across
> Isabelle/Pure and Isabelle/HOL.  Can someone direct me to a listing of
> all the rules and axioms?

in addition to Larry's reply, and running the risk that I'm pointing out
the obvious:  the (implementation of the) inference rules of Isabelle's
meta logic may be found in src/Pure/thm.ML (see


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