IDE: Introduction, Destruction, Elimination

Mihails Milehins 📧

September 6, 2021

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


The article provides the command mk_ide for the object logic Isabelle/HOL of the formal proof assistant Isabelle. The command mk_ide enables the automated synthesis of the introduction, destruction and elimination rules from arbitrary definitions of constant predicates stated in Isabelle/HOL.


BSD License


Session Intro_Dest_Elim