src/Pure/pattern.ML
changeset 31157 6e1e8e194562
parent 30565 784be11cb70e
child 32032 a6a6e8031c14