src/HOL/Metis.thy
changeset 82314 c95eca07f6a0
parent 81254 d3c0734059ee