src/HOL/IMP/Denotation.ML
changeset 4572 a259399ac328
parent 4477 b3e5857d8d99
child 5069 3ea049f7979d