src/HOL/Metis.thy
changeset 82407 fcc0f74ac086
parent 81254 d3c0734059ee