src/HOL/ex/Code_Timing.thy
changeset 71370 b05aca9cee75
parent 69597 ff784d5a5bfb
equal deleted inserted replaced
71369:897ff7e68a10 71370:b05aca9cee75