src/HOL/Extraction.thy
changeset 83134 22b9bd48d270
parent 70847 e62d5433bb47
equal deleted inserted replaced
83133:cd0bc60a8258 83134:22b9bd48d270