src/HOL/ex/Simps_Case_Conv_Examples.thy
changeset 74737 d912c1b6c1d0
parent 69568 de09a7261120