src/HOL/HOL.thy
changeset 23024 70435ffe077d
parent 22993 838c66e760b5
child 23037 6c72943a71b1