src/HOL/Library/Simps_Case_Conv.thy
changeset 65380 ae93953746fc
parent 63582 161c5d8ae266
child 67013 335a7dce7cb3