src/Pure/General/history.ML
changeset 8413 09db77a084aa
parent 7715 f90ec7937a7d
child 8806 a202293db3f6
equal deleted inserted replaced
8412:65f9089f6f71 8413:09db77a084aa