*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] What are the Rules and Axioms of Isabelle/HOL Exactly?*From*: Matthew Wampler-Doty <negacthulhu at gmail.com>*Date*: Thu, 14 Jan 2010 02:16:14 +0100

Dear all, 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? Thanks! ~Matthew P. Wampler-Doty

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

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

- Previous by Date: [isabelle] Two PhD positions in theoretical computer science
- Next by Date: Re: [isabelle] What are the Rules and Axioms of Isabelle/HOL Exactly?
- Previous by Thread: [isabelle] Two PhD positions in theoretical computer science
- 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