src/HOL/IMP/Denotation.thy
changeset 4102 f746af27164b
parent 2847 6226b83ce2d8
child 4897 be11be0b6ea1