Mario Xerxes Castelán Castro (Dec 25 2025 at 03:58): Mario Xerxes Castelán Castro (Dec 25 2025 at 03:58):Is "Pure" the native logic of Isabelle? By "native" I mean the one the kernel directly operates on.
Mario Xerxes Castelán Castro (Dec 25 2025 at 04:07):I found it is. Does Pure have a manual?
Kevin Kappelmann (Dec 26 2025 at 07:48):What topics are you interested in? Maybe section 2.1 in the isar reference manual
https://isabelle.in.tum.de/dist/Isabelle2025-1/doc/isar-ref.pdf
and it's cited sources [45,46] are what you are looking for.
Last updated: Dec 28 2025 at 02:03 UTC