# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1727886756 -7200
# Node ID 28ef01901650e95601ae2124cb43054ecc3d460a
# Parent  e0327a38bf4dd30650c613aa41e57849fa01ba9d
proper command kinds;

diff -r e0327a38bf4d -r 28ef01901650 src/HOL/Data_Structures/Define_Time_Function.thy
--- a/src/HOL/Data_Structures/Define_Time_Function.thy	Wed Oct 02 13:51:45 2024 +0200
+++ b/src/HOL/Data_Structures/Define_Time_Function.thy	Wed Oct 02 18:32:36 2024 +0200
@@ -10,8 +10,8 @@
 theory Define_Time_Function
   imports Main
   keywords "time_fun" :: thy_decl
-    and    "time_function" :: thy_goal
-    and    "time_definition" :: thy_goal
+    and    "time_function" :: thy_decl
+    and    "time_definition" :: thy_decl
     and    "equations"
     and    "time_fun_0" :: thy_decl
 begin