src/Pure/tactic.ML
changeset 5253 82a5ca6290aa
parent 4713 bea2ab2e360b
child 5263 8862ed2db431