src/HOL/Extraction.thy
changeset 27885 76b51cd0a37c
parent 25424 170f4cc34697
child 27982 2aaa4a5569a6
equal deleted inserted replaced
27884:10c927e4abf5 27885:76b51cd0a37c