src/Pure/tactic.ML
changeset 77591 3f3dcf9f53f1
parent 74282 c2ee8d993d6a