src/Pure/tactic.ML
changeset 80778 94bc8f62c835
parent 74282 c2ee8d993d6a
child 82805 61aae966dd95
equal deleted inserted replaced
80776:3a9e570c916d 80778:94bc8f62c835