src/Pure/consts.ML
changeset 78810 9473dd79e9c3
parent 77979 a12c48fbf10f
child 79449 e6fb110d6e44
equal deleted inserted replaced
78809:76ab04bca48c 78810:9473dd79e9c3