Sat, 20 May 2023 22:41:37 +0200 tuned signature;
wenzelm [Sat, 20 May 2023 22:41:37 +0200] rev 78090
tuned signature;
Sat, 20 May 2023 21:48:41 +0200 tuned;
wenzelm [Sat, 20 May 2023 21:48:41 +0200] rev 78089
tuned;
Sat, 20 May 2023 21:23:44 +0200 tuned --- Token.make_string / Token.assign are value-oriented;
wenzelm [Sat, 20 May 2023 21:23:44 +0200] rev 78088
tuned --- Token.make_string / Token.assign are value-oriented;
Sat, 20 May 2023 20:56:13 +0200 more documentation;
wenzelm [Sat, 20 May 2023 20:56:13 +0200] rev 78087
more documentation;
Sat, 20 May 2023 17:42:01 +0200 tuned signature;
wenzelm [Sat, 20 May 2023 17:42:01 +0200] rev 78086
tuned signature;
Sat, 20 May 2023 17:18:44 +0200 tuned signature;
wenzelm [Sat, 20 May 2023 17:18:44 +0200] rev 78085
tuned signature;
Sat, 20 May 2023 16:12:37 +0200 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 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);
Sat, 20 May 2023 14:48:06 +0200 prefer static simpset;
wenzelm [Sat, 20 May 2023 14:48:06 +0200] rev 78083
prefer static simpset;
Sat, 20 May 2023 14:12:01 +0200 omit pointless morphism in global theory;
wenzelm [Sat, 20 May 2023 14:12:01 +0200] rev 78082
omit pointless morphism in global theory;
Sat, 20 May 2023 12:04:41 +0200 more operations;
wenzelm [Sat, 20 May 2023 12:04:41 +0200] rev 78081
more operations;
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 tip