src/Pure/context.ML
changeset 78810 9473dd79e9c3
parent 78464 12af46f2cd94
child 79076 a1b5357b5473
equal deleted inserted replaced
78809:76ab04bca48c 78810:9473dd79e9c3