src/HOL/Extraction.thy
changeset 32047 c141f139ce26
parent 30235 58d147683393
child 33704 6aeb8454efc1
equal deleted inserted replaced
32045:efc5f4806cd5 32047:c141f139ce26