src/HOL/Library/simps_case_conv.ML
changeset 78134 a11ebc8c751a
parent 74529 a1aa42743d7d
child 79733 3e30ca77ccfe