Interactive Simplifier Tracing and Debugging in Isabelle

DOI10.1007/978-3-319-08434-3_24zbMath1304.68156arXiv1406.0292OpenAlexW3102762027WikidataQ57955192 ScholiaQ57955192MaRDI QIDQ5495933

Lars Hupel

Publication date: 7 August 2014

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

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

zbMATH Keywords

term rewritingdebuggingtracingIsabellesimplifier

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (1)

Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC

Uses Software

• Isabelle
• Isabelle/Isar
• Isar
• Proof General
• Maude
• PIDE
• Isabelle/jEdit
• Sledgehammer
• jEdit
• iJulienne
• Poly/ML
• GDB

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Isabelle/jEdit – A Prover IDE within the PIDE Framework
• Automatic Proof and Disproof in Isabelle/HOL
• Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit

This page was built for publication: Interactive Simplifier Tracing and Debugging in Isabelle