src/Pure/tactic.ML
changeset 16352 d7f9978e5752
parent 16325 a6431098a929
child 16425 2427be27cc60