src/Pure/ROOT.ML
changeset 20147 7aa076a45cb4
parent 20075 a7e183bfebef
child 20207 4c57e850e8d5
equal deleted inserted replaced
20146:d8cf6eb9baf9 20147:7aa076a45cb4