src/Pure/tctical.ML
changeset 3257 4e3724e0659f
parent 2807 04c080e60f31
child 3561 329441e7eeee
equal deleted inserted replaced
3256:0a45cdd7da37 3257:4e3724e0659f