src/HOL/Library/Simps_Case_Conv.thy
changeset 63558 0aa33085c8b1
parent 63432 ba7901e94e7b
child 63579 73939a9b70a3