(* Title: HOL/Datatype_Examples/Simproc_Tests.thy Author: Manuel Eberl, TU München *) section ‹Tests of datatype-specific simprocs› theory Datatype_Simproc_Tests imports Main begin (* datatype without parameters *) datatype foo = X | Y foo foo lemma "x ≠ Y x y" "x ≠ Y y x" "Y x y ≠ x" "Y y x ≠ x" by simp_all (* datatype with parameters *)