changeset 79969 | 4aeb25ba90f3 |
parent 79495 | 8a2511062609 |
--- a/src/HOL/Data_Structures/Queue_2Lists.thy Sun Mar 24 14:15:10 2024 +0100 +++ b/src/HOL/Data_Structures/Queue_2Lists.thy Sun Mar 24 14:50:47 2024 +0100 @@ -59,10 +59,10 @@ text \<open>Running times:\<close> -define_time_fun norm -define_time_fun enq -define_time_fun tl -define_time_fun deq +time_fun norm +time_fun enq +time_fun tl +time_fun deq lemma T_tl_0: "T_tl xs = 0" by(cases xs)auto