src/HOL/Data_Structures/Queue_2Lists.thy

--- a/src/HOL/Data_Structures/Queue_2Lists.thy	Tue Nov 05 23:51:44 2024 +0100
+++ b/src/HOL/Data_Structures/Queue_2Lists.thy	Wed Nov 06 16:19:45 2024 +0100
@@ -5,7 +5,7 @@
 theory Queue_2Lists
 imports
   Queue_Spec
-  Reverse
+  Time_Funs
 begin
 
 text \<open>Definitions:\<close>
@@ -61,12 +61,8 @@
 
 time_fun norm
 time_fun enq
-time_fun tl
 time_fun deq
 
-lemma T_tl_0: "T_tl xs = 0"
-by(cases xs)auto
-
 text \<open>Amortized running times:\<close>
 
 fun \<Phi> :: "'a queue \<Rightarrow> nat" where
@@ -76,6 +72,6 @@
 by(auto simp: T_itrev)
 
 lemma a_deq: "T_deq (fs,rs) + \<Phi>(deq (fs,rs)) - \<Phi>(fs,rs) \<le> 1"
-by(auto simp: T_itrev T_tl_0)
+by(auto simp: T_itrev T_tl)
 
 end