src/HOL/Isar_examples/ExprCompiler.thy
changeset 14544 2d0c4c5819d3
parent 13537 f506eb568121
child 16417 9bc16273c2d4
equal deleted inserted replaced
14543:0e266a5dd6e3 14544:2d0c4c5819d3