src/Pure/ROOT.ML
changeset 18916 fda5b8dbbef6
parent 18870 020e242c02a0
child 18934 0342b7c21388
equal deleted inserted replaced
18915:7521b849ae98 18916:fda5b8dbbef6