src/HOL/Predicate_Compile_Examples/IMP_1.thy
changeset 67613 ce654b0e6d69
parent 66453 cc19f7ca2ed6