src/Pure/ROOT.ML
changeset 69805 a8debe27c36c
parent 69449 b516fdf8005c
child 69876 b49bd228ac8a
equal deleted inserted replaced
69804:9efccbad7d42 69805:a8debe27c36c