Structured Induction Proofs in Isabelle/Isar

DOI10.1007/11812289_3zbMATH Open1188.68266OpenAlexW1583435594MaRDI QIDQ5756773FDOQ5756773

Authors: Makarius Wenzel 

Publication date: 5 September 2007

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

Full work available at URL: https://doi.org/10.1007/11812289_3

Recommendations

• Logic-Free Reasoning in Isabelle/Isar
• The Isabelle Framework
• scientific article; zbMATH DE number 1863378
• Interactive theorem proving from the perspective of Isabelle/Isar
• Building Formal Method Tools in the Isabelle/Isar Framework

Mathematics Subject Classification ID

Computing methodologies for text processing; mathematical typography (68U15)

Cited In (7)

• Building Formal Method Tools in the Isabelle/Isar Framework
• The Isabelle Framework
• Eisbach: a proof method language for Isabelle
• Types for Proofs and Programs
• The equational part of proofs by structural induction
• Title not available (Why is that?)
• Nominal techniques in Isabelle/HOL

Uses Software

• Isabelle
• Isabelle/Isar
• Isar

This page was built for publication: Structured Induction Proofs in Isabelle/Isar

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5756773)