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