src/HOL/ex/Code_Timing.thy
changeset 80157 6b9d5cae4579
parent 69597 ff784d5a5bfb
equal deleted inserted replaced
80156:70d69b081561 80157:6b9d5cae4579