src/Pure/NJ.ML
changeset 1390 bf523422a3df
parent 1289 2edd7a39d92a
child 1480 85ecd3439e01
equal deleted inserted replaced
1389:fbe857ddc80d 1390:bf523422a3df