src/HOL/HOL.ML
changeset 2559 06b6a499f8ae
parent 2442 6663e0d210b0
child 2562 d571d6660240
equal deleted inserted replaced
2558:6e8d130463e3 2559:06b6a499f8ae