The following pages link to Equational reasoning in Isabelle (Q1825045):
Displaying 17 items.
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- Eisbach: a proof method language for Isabelle (Q287365) (← links)
- Term rewriting and beyond -- theorem proving in Isabelle (Q909488) (← links)
- Equational methods in first order predicate calculus (Q1065783) (← links)
- Introduction to ``Milestones in interactive theorem proving'' (Q1663212) (← links)
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols (Q2424886) (← links)
- (Q2754042) (← links)
- Equational Reasoning with Applicative Functors (Q2829262) (← links)
- Tactics for Reasoning Modulo AC in Coq (Q3100211) (← links)
- Interactive proof-search for equational reasoning (Q3386920) (← links)
- The Isabelle Framework (Q3543647) (← links)
- (Q3750118) (← links)
- (Q4362899) (← links)
- Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL (Q5049005) (← links)
- Computer Science Logic (Q5311286) (← links)
- Logic-Free Reasoning in Isabelle/Isar (Q5505517) (← links)
- The practice of logical frameworks (Q5878905) (← links)