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

On Thu, Jan 14, 2010 at 4:49 PM, Tjark Weber <webertj at> wrote:
> Matthew,
> 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

Oh, I probably really should have looked here first before posting...

Thank you all for your kind replies!


> Regards,
> Tjark

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