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