thys/Hoare_tm2.thy
changeset 24 77daf1b85cf0
parent 19 087d82632852