src/HOL/ex/Code_Timing.thy
changeset 80582 1bc7eef961ff
parent 69597 ff784d5a5bfb