src/HOL/IMP/Denotation.thy
changeset 3895 b2463861c86a
parent 2847 6226b83ce2d8
child 4897 be11be0b6ea1