src/HOL/HOL.thy
changeset 22871 9ffb43b19ec6
parent 22839 ede26eb5e549
child 22993 838c66e760b5