src/HOL/HOL.ML
changeset 2754 59bd96046ad6
parent 2562 d571d6660240
child 3003 c5293a17afa6
equal deleted inserted replaced
2753:bcde71e5f371 2754:59bd96046ad6