src/HOL/Predicate_Compile_Examples/IMP_1.thy
changeset 68211 1e7defef8c8a
parent 66453 cc19f7ca2ed6
equal deleted inserted replaced
68210:65f79c0ddb0d 68211:1e7defef8c8a