src/HOL/IMP/Denotation.thy
changeset 8039 a901bafe4578
parent 5608 a82a038a3e7a
child 9241 f961c1fdff50