src/HOL/ex/Simps_Case_Conv_Examples.thy
changeset 72508 c89d8e8bd8c7
parent 69568 de09a7261120