IDE: Introduction, Destruction, Elimination

Mihails Milehins 📧

September 6, 2021

Abstract

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

Topics

Theories of Intro_Dest_Elim