wenzelm [Sat, 20 May 2023 21:48:41 +0200] rev 78089
tuned;
wenzelm [Sat, 20 May 2023 21:23:44 +0200] rev 78088
tuned --- Token.make_string / Token.assign are value-oriented;
wenzelm [Sat, 20 May 2023 20:56:13 +0200] rev 78087
more documentation;
wenzelm [Sat, 20 May 2023 17:42:01 +0200] rev 78086
tuned signature;
wenzelm [Sat, 20 May 2023 17:18:44 +0200] rev 78085
tuned signature;
wenzelm [Sat, 20 May 2023 16:12:37 +0200] rev 78084
more robust context: fail immediately via Morphism.the_theory, instead of rarely via Thm.theory_of_thm (for non-normal thm);
wenzelm [Sat, 20 May 2023 14:48:06 +0200] rev 78083
prefer static simpset;
wenzelm [Sat, 20 May 2023 14:12:01 +0200] rev 78082
omit pointless morphism in global theory;
wenzelm [Sat, 20 May 2023 12:04:41 +0200] rev 78081
more operations;
wenzelm [Fri, 19 May 2023 22:09:06 +0200] rev 78080
more careful treatment of context for method source;
wenzelm [Fri, 19 May 2023 21:48:11 +0200] rev 78079
clarified context;
wenzelm [Fri, 19 May 2023 21:22:39 +0200] rev 78078
clarified signature;
wenzelm [Fri, 19 May 2023 11:42:12 +0200] rev 78077
remove pointless context setup (see also b2e449c155a4);
wenzelm [Fri, 19 May 2023 11:41:30 +0200] rev 78076
more careful reset_context for stored entity;
wenzelm [Thu, 18 May 2023 23:50:59 +0200] rev 78075
more careful reset/set_context for stored declarations;
wenzelm [Thu, 18 May 2023 23:21:05 +0200] rev 78074
tuned;
wenzelm [Thu, 18 May 2023 23:20:41 +0200] rev 78073
tuned;
wenzelm [Thu, 18 May 2023 17:21:29 +0200] rev 78072
clarified signature: more explicit types;
wenzelm [Thu, 18 May 2023 15:34:01 +0200] rev 78071
clarified data: avoid pointless Morphism.transform;
wenzelm [Thu, 18 May 2023 14:06:35 +0200] rev 78070
proper Token.Declaration for internal_declaration;
wenzelm [Tue, 16 May 2023 20:26:09 +0200] rev 78069
more standard treatment of morphism context;
wenzelm [Tue, 16 May 2023 19:52:50 +0200] rev 78068
tuned: avoid duplication;
wenzelm [Tue, 16 May 2023 19:43:42 +0200] rev 78067
more standard treatment of morphism context, but hardly relevant here;
wenzelm [Tue, 16 May 2023 19:42:19 +0200] rev 78066
tuned;