src/HOL/IMP/Denotation.thy
changeset 4386 b3cff8adc213
parent 2847 6226b83ce2d8
child 4897 be11be0b6ea1