src/Pure/pattern.ML
changeset 30911 7809cbaa1b61
parent 30565 784be11cb70e
child 32032 a6a6e8031c14
equal deleted inserted replaced
30910:a7cc0ef93269 30911:7809cbaa1b61