src/HOL/Metis.thy
changeset 81350 1818358373e2
parent 81254 d3c0734059ee