src/HOL/ex/Codegenerator.thy
changeset 24245 4ffeb1dd048a
parent 24195 7d1a16c77f7c
child 24249 1f60b45c5f97