src/HOL/Data_Structures/Time_Funs.thy

--- a/src/HOL/Data_Structures/Time_Funs.thy	Mon Mar 25 17:55:02 2024 +0100
+++ b/src/HOL/Data_Structures/Time_Funs.thy	Wed Mar 27 16:48:23 2024 +0100
@@ -7,6 +7,11 @@
   imports Define_Time_Function
 begin
 
+time_fun "(@)"
+
+lemma T_append: "T_append xs ys = length xs + 1"
+by(induction xs) auto
+
 text \<open>Automatic definition of \<open>T_length\<close> is cumbersome because of the type class for \<open>size\<close>.\<close>
 
 fun T_length :: "'a list \<Rightarrow> nat" where