src/HOL/Isar_examples/ExprCompiler.thy
changeset 7260 745f834281e2
parent 7253 a494a78fea39
child 7480 0a0e0dbe1269
equal deleted inserted replaced
7259:e75aa311788c 7260:745f834281e2