src/Pure/defs.ML
changeset 33951 651028e34b5d
parent 33712 cffc97238102
child 35845 e5980f0ad025
equal deleted inserted replaced
33950:0a77b979e593 33951:651028e34b5d