src/HOL/Library/simps_case_conv.ML
changeset 79556 0631dfc0db07
parent 74529 a1aa42743d7d
child 79733 3e30ca77ccfe