Fri, 14 Oct 2022 13:35:25 +0200 proper Symbol.encode (following fd1efd6dd385), e.g. relevant for 'ML_file' with symbols like \<^here>;
wenzelm [Fri, 14 Oct 2022 13:35:25 +0200] rev 76307
proper Symbol.encode (following fd1efd6dd385), e.g. relevant for 'ML_file' with symbols like \<^here>;
Tue, 18 Oct 2022 07:57:30 +0200 merged
desharna [Tue, 18 Oct 2022 07:57:30 +0200] rev 76306
merged
Mon, 17 Oct 2022 18:21:54 +0200 added lemma fmember_iff_member_fset
desharna [Mon, 17 Oct 2022 18:21:54 +0200] rev 76305
added lemma fmember_iff_member_fset
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 tip