src/HOL/Predicate_Compile_Examples/IMP_3.thy
changeset 39586 ea8f3ea13a95
parent 39249 9c866b248cb1
child 40924 a9be7f26b4e6