src/HOL/HOL.ML
changeset 4349 50403e5a44c0
parent 4302 2c99775d953f
child 4467 bd05e2a28602
equal deleted inserted replaced
4348:c7f6b4256964 4349:50403e5a44c0