src/HOL/HOL.thy
changeset 27125 0733f575b51e
parent 27107 4a7415c67063
child 27126 3ede9103de8e