src/HOL/HOL.ML
changeset 1444 23ceb1dc9755
parent 1338 d2fc3bfaee7f
child 1455 52a0271621f3