src/HOL/Predicate_Compile_Examples/IMP_2.thy
changeset 40932 b9f56b4025d2
parent 40924 a9be7f26b4e6
child 41413 64cd30d6b0b8