src/HOLCF/ex/Focus_ex.ML
changeset 12372 cd3a09c7dac9
parent 12036 49f6c49454c2
child 12525 4ad978c8f550
equal deleted inserted replaced
12371:80ca9058db95 12372:cd3a09c7dac9