Proof presentation for Isabelle
- 1 January 1997
- book chapter
- Published by Springer Nature
- p. 259-274
- https://doi.org/10.1007/bfb0028399
Abstract
No abstract availableKeywords
This publication has 14 references indexed in Scilit:
- More Church-Rosser proofs (in Isabelle/HOL)Published by Springer Nature ,1996
- How to Write a ProofThe American Mathematical Monthly, 1995
- The calculational methodInformation Processing Letters, 1995
- Annotations in formal specifications and proofsFormal Methods in System Design, 1994
- IsabellePublished by Springer Nature ,1994
- A Logical Approach to Discrete MathPublished by Springer Nature ,1993
- Predicate Calculus and Program SemanticsPublished by Springer Nature ,1990
- Literate ProgrammingThe Computer Journal, 1984
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting SystemsJournal of the ACM, 1980
- Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theoremIndagationes Mathematicae, 1972