src/HOL/Library/simps_case_conv.ML
changeset 77537 1bbf29ec9ce3
parent 74529 a1aa42743d7d
child 79733 3e30ca77ccfe