src/HOL/IMP/Expr.thy
changeset 39666 4f628ee48fd7
parent 37736 2bf3a2cb5e58
child 41589 bbd861837ebc