Stream: Beginner Questions

Topic: Axiom schemas in Isabelle

view this post on Zulip Lekhani Ray (Aug 25 2022 at 14:55):

Is there a direct way to formalize axiom schemas in Isabelle?

view this post on Zulip Mathias Fleury (Aug 30 2022 at 07:46):

Maybe look at how other people are doing it in the AFP? E.g. https://www.isa-afp.org/theories/axiomaticcategorytheory/#AxiomaticCategoryTheory?

view this post on Zulip Lawrence Paulson (Aug 31 2022 at 14:29):

If you mean axioms containing a formula variable, just type it in. But it's unwise to assume axioms unless you really know what you are doing. 1=0 is never far away.

Last updated: Dec 21 2024 at 16:20 UTC