src/HOL/HOL.thy
changeset 25277 95128fcdd7e8
parent 25062 af5ef0d4d655
child 25297 a5d689d04426