proper command kinds;
authorFabian Huch <huch@in.tum.de>
Wed, 02 Oct 2024 18:32:36 +0200
changeset 81088 28ef01901650
parent 81087 e0327a38bf4d
child 81108 92768949a923
proper command kinds;
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