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



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





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