src/HOL/Extraction.thy
changeset 14747 2eaff69d3d10
parent 14168 ed81cd283816
child 14981 e73f8140af78
equal deleted inserted replaced
14746:9f7b31cf74d8 14747:2eaff69d3d10