src/HOL/HOL.thy
changeset 27123 11fcdd5897dd
parent 27107 4a7415c67063
child 27126 3ede9103de8e