src/Pure/basis.ML
changeset 12671 bb6db6c0d4df
parent 11852 a528a716a312
child 13037 f7f29f8380ce
equal deleted inserted replaced
12670:5c896eccb290 12671:bb6db6c0d4df