src/HOL/IMP/Denotational.thy
changeset 80730 be4c1fbccfe8
parent 69661 a03a63b81f44
equal deleted inserted replaced
80729:dff10bb4ebdb 80730:be4c1fbccfe8