src/HOL/HOL.thy
changeset 14255 e6e3e3f0deed
parent 14248 399a3290936c
child 14295 7f115e5c5de4