src/Pure/pattern.ML
changeset 23024 70435ffe077d
parent 22678 23963361278c
child 23222 daca4731942f