src/Pure/pattern.ML
changeset 47747 47d1ffdbb6e7
parent 46857 628b4a3fbf6e
child 51700 c8f2bad67dbb