src/Pure/tactic.ML
changeset 17740 fc385ce6187d
parent 17496 26535df536ae
child 17851 2fa4f9b54761
equal deleted inserted replaced
17739:eddebb044a62 17740:fc385ce6187d