Isabelle as Document-Oriented Proof Assistant

DOI10.1007/978-3-642-22673-1_17zbMath1335.68239OpenAlexW76860425MaRDI QIDQ5200122

Makarius Wenzel

Publication date: 29 July 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22673-1_17

Mathematics Subject Classification ID

Knowledge representation (68T30)

Related Items

Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface ⋮ From LCF to Isabelle/HOL ⋮ Translating Scala Programs to Isabelle/HOL

Uses Software

• Coq
• Isabelle
• Proviola
• Isabelle/HOL
• Isar
• Proof General
• Matita
• Isabelle/jEdit
• Scala
• Proof General Kit
• Pcoq

Cites Work

• Unnamed Item
• User interaction with the Matita proof assistant
• PlatΩ: A Mediator between Text-Editors and Proof Assistance Systems
• Proviola: A Tool for Proof Re-animation
• Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit
• A Framework for Interactive Proof
• Mathematical Knowledge Management