src/HOL/HOL.thy
changeset 5104 230cca8452c7
parent 5069 3ea049f7979d
child 5186 439e292b5b87