src/HOL/HOL.thy
changeset 26100 fbc60cd02ae2
parent 25966 74f6817870f9
child 26411 cd74690f3bfb