src/HOL/Metis.thy
changeset 58002 0ed1e999a0fb
parent 56946 10d9bd4ea94f
child 58818 ee85e7b82d00