src/HOL/Tools/Function/pattern_split.ML
changeset 33629 5f35cf91c6a4
parent 33099 b8cdd3d73022
child 33855 cd8acf137c9c
equal deleted inserted replaced
33628:ed2111a5c3ed 33629:5f35cf91c6a4