src/HOL/HOL.thy
changeset 2981 aa5aeb6467c6
parent 2912 3fac3e8d5d3e
child 3066 3c548f92e032