src/HOL/Metis.thy
changeset 81275 5ed639c16ce7
parent 81254 d3c0734059ee