src/HOL/Tools/Function/pattern_split.ML
changeset 33020 0908ed080ccf
parent 32952 aeb1e44fbc19
child 33037 b22e44496dc2