src/HOL/Library/Simps_Case_Conv.thy
changeset 77554 4465d9dff448
parent 69605 a96320074298