src/HOL/Extraction.thy
changeset 60243 5901cb4db0ae
parent 60070 73c6e58a105c
child 60147 6d7b7a037e8d