src/HOL/Isar_examples/ExprCompiler.thy
changeset 7990 0a604b2fc2b1
parent 7982 d534b897ce39
child 8031 826c6222cca2