src/HOL/Predicate_Compile_Examples/IMP_4.thy
changeset 39625 fb0c851e4f9d
parent 39186 475856793715
child 40924 a9be7f26b4e6