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



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).

Regards,
Tjark






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