src/HOL/Extraction.thy
changeset 36970 fb3fdb4b585e
parent 34913 d8cb720c9c53
child 37233 b78f31ca4675
equal deleted inserted replaced
36964:a354605f03dc 36970:fb3fdb4b585e