Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Data_Structures/Time_Funs.thy
changeset 79969 4aeb25ba90f3
parent 79495 8a2511062609
child 80036 a594d22e69d6 
--- a/src/HOL/Data_Structures/Time_Funs.thy	Sun Mar 24 14:15:10 2024 +0100
+++ b/src/HOL/Data_Structures/Time_Funs.thy	Sun Mar 24 14:50:47 2024 +0100
@@ -48,8 +48,8 @@
 
 lemmas [simp del] = T_nth.simps
 
-define_time_fun take
-define_time_fun drop
+time_fun take
+time_fun drop
 
 lemma T_take_eq: "T_take n xs = min n (length xs) + 1"
   by (induction xs arbitrary: n) (auto split: nat.splits)
isabelle