src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
changeset 57426 2cd2ccd81f93
parent 50630 1ea90e8046dc
child 58889 5b7a9633cfa8