src/Pure/tactic.ML
changeset 73149 bdc8cd6f5e6e
parent 69101 991a3feaf270
child 74282 c2ee8d993d6a
equal deleted inserted replaced
73148:5f49f1149c1c 73149:bdc8cd6f5e6e