src/HOL/Isar_examples/ExprCompiler.thy
changeset 9502 50ec59aff389
parent 8304 e132d147374b
child 9659 b9cf6801f3da