src/Pure/tactic.ML
changeset 12472 3307149f1ec2
parent 12320 6e70d870ddf0
child 12498 3b0091bf06e8
equal deleted inserted replaced
12471:632cb16dc07e 12472:3307149f1ec2