*To*: Matthew Wampler-Doty <negacthulhu at gmail.com>*Subject*: Re: [isabelle] What are the Rules and Axioms of Isabelle/HOL Exactly?*From*: Tjark Weber <webertj at in.tum.de>*Date*: Thu, 14 Jan 2010 15:49:40 +0000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <afdf13fb1001131716xfeeba0ehc41b6cb0a3387ae2@mail.gmail.com>*References*: <afdf13fb1001131716xfeeba0ehc41b6cb0a3387ae2@mail.gmail.com>

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

**Follow-Ups**:**Re: [isabelle] What are the Rules and Axioms of Isabelle/HOL Exactly?***From:*Matthew Wampler-Doty

**References**:**[isabelle] What are the Rules and Axioms of Isabelle/HOL Exactly?***From:*Matthew Wampler-Doty

- Previous by Date: Re: [isabelle] What are the Rules and Axioms of Isabelle/HOL Exactly?
- Next by Date: Re: [isabelle] What are the Rules and Axioms of Isabelle/HOL Exactly?
- Previous by Thread: Re: [isabelle] What are the Rules and Axioms of Isabelle/HOL Exactly?
- Next by Thread: Re: [isabelle] What are the Rules and Axioms of Isabelle/HOL Exactly?
- Cl-isabelle-users January 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list