src/HOL/Tools/Function/pattern_split.ML
changeset 32970 fbd2bb2489a8
parent 32952 aeb1e44fbc19
child 33037 b22e44496dc2