src/HOL/Imperative_HOL/Imperative_HOL_ex.thy
changeset 31409 d8537ba165b5
parent 30694 4b182a031731
child 31872 a564aca741f2