src/HOL/Tools/function_package/pattern_split.ML
changeset 20535 b4b3933ec026
parent 20523 36a59e5d0039
child 20636 ddddf0b7d322