src/HOL/Library/Simps_Case_Conv.thy
changeset 65210 8cfdf420b643
parent 63582 161c5d8ae266
child 67013 335a7dce7cb3