src/HOL/HOLCF/IMP/HoareEx.thy
changeset 80946 b76f64d7d493
parent 80914 d97fdabd9e2b