Interaction with formal mathematical documents in Isabelle/PIDE

DOI10.1007/978-3-030-23250-4_1zbMath1428.68347arXiv1905.01735MaRDI QIDQ2287890

Makarius Wenzel

Publication date: 22 January 2020

Full work available at URL: https://arxiv.org/abs/1905.01735

Mathematics Subject Classification ID

68V20: Formalization of mathematics in connection with theorem provers

68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Uses Software

• Coq
• Isabelle/HOL
• Isabelle/Isar
• Proof General
• PIDE
• Isabelle/jEdit
• Sledgehammer
• Isabelle/PIDE
• Archive Formal Proofs