src/HOL/ex/Codegenerator.thy
changeset 24433 4a405457e9d6
parent 24432 d555d941f983
child 24718 16b11ba36350