src/HOL/Extraction.thy
changeset 73215 a81ec42bac45
parent 70847 e62d5433bb47
equal deleted inserted replaced
73214:5de4a6ae6065 73215:a81ec42bac45