src/HOL/HOL.thy
changeset 28157 0435d23deccc
parent 28054 2b84d34c5d02
child 28227 77221ee0f7b9