src/HOL/Metis.thy
changeset 57978 8f4a332500e4
parent 56946 10d9bd4ea94f
child 58818 ee85e7b82d00