src/HOL/IMP/Denotation.ML
changeset 1868 836950047d85
parent 1731 2ad693c6cb13
child 1973 8c94c9a5be10