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 in.tum.de> 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
> http://isabelle.in.tum.de/repos/isabelle/file/a22b09addd78/src/Pure/thm.ML).

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

Thank you all for your kind replies!

~Matt

> Regards,
> Tjark
>
>





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