src/Pure/pattern.ML
changeset 4932 c90411dde8e8
parent 4820 8f6dbbd8d497
child 6539 2e7d2fba9f6c
equal deleted inserted replaced
4931:2ec84dee7911 4932:c90411dde8e8