src/HOL/IMP/Denotation.thy
changeset 8993 cbfebff56cc0
parent 5608 a82a038a3e7a
child 9241 f961c1fdff50