src/HOL/Library/Simps_Case_Conv.thy
changeset 68343 2941e58318c7
parent 67724 63e305429f8a
child 69568 de09a7261120