src/HOL/Library/simps_case_conv.ML
changeset 77290 12fd873af77c
parent 74529 a1aa42743d7d
child 79733 3e30ca77ccfe