src/HOL/Metis.thy
changeset 80900 2c75875ccf94
parent 78728 72631efa3821
child 81254 d3c0734059ee