src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
changeset 76044 c90799513ed0
parent 72671 588c751a5eef