src/HOL/HOL.ML
changeset 4176 84a0bfbd74e5
parent 4131 916641b59219
child 4302 2c99775d953f
equal deleted inserted replaced
4175:06774cd43054 4176:84a0bfbd74e5