changeset 79969 | 4aeb25ba90f3 |
parent 79490 | b287510a4202 |
--- a/src/HOL/Data_Structures/Define_Time_0.ML Sun Mar 24 14:15:10 2024 +0100 +++ b/src/HOL/Data_Structures/Define_Time_0.ML Sun Mar 24 14:50:47 2024 +0100 @@ -37,7 +37,7 @@ end val _ = - Outer_Syntax.command \<^command_keyword>\<open>define_time_0\<close> "ML setup for global theory" + Outer_Syntax.command \<^command_keyword>\<open>time_fun_0\<close> "ML setup for global theory" (Parse.prop >> (Toplevel.theory o save)); end \ No newline at end of file