src/HOL/Extraction.thy
changeset 72569 d56e4eeae967
parent 70847 e62d5433bb47
equal deleted inserted replaced
72568:bac8921e2901 72569:d56e4eeae967