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