Thu, 09 Nov 2023 11:30:33 +0100 proper local host (amending 62d7ef1da441);
wenzelm [Thu, 09 Nov 2023 11:30:33 +0100] rev 78924
proper local host (amending 62d7ef1da441);
Wed, 08 Nov 2023 21:45:02 +0100 merged
nipkow [Wed, 08 Nov 2023 21:45:02 +0100] rev 78923
merged
Wed, 08 Nov 2023 21:44:44 +0100 added lemma
nipkow [Wed, 08 Nov 2023 21:44:44 +0100] rev 78922
added lemma
Wed, 08 Nov 2023 20:31:29 +0100 proper default for disjunction (amending 9f7a94117666);
wenzelm [Wed, 08 Nov 2023 20:31:29 +0100] rev 78921
proper default for disjunction (amending 9f7a94117666);
Wed, 08 Nov 2023 19:04:44 +0100 tuned;
wenzelm [Wed, 08 Nov 2023 19:04:44 +0100] rev 78920
tuned;
Wed, 08 Nov 2023 16:05:22 +0100 more operations;
wenzelm [Wed, 08 Nov 2023 16:05:22 +0100] rev 78919
more operations;
Wed, 08 Nov 2023 15:37:15 +0100 avoid option -C: free this latter for build-related configuration;
wenzelm [Wed, 08 Nov 2023 15:37:15 +0100] rev 78918
avoid option -C: free this latter for build-related configuration;
Wed, 08 Nov 2023 15:10:19 +0100 more direct indentation, using Symbol.spaces;
wenzelm [Wed, 08 Nov 2023 15:10:19 +0100] rev 78917
more direct indentation, using Symbol.spaces;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -8 +8 +10 +30 +100 +300 +1000 tip