src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
changeset 82276 d22e9c5b5dc6
parent 72671 588c751a5eef