# HG changeset patch
# User wenzelm
# Date 1727811059 -7200
# Node ID c92efbf32bfea1cf28e26267457d3320a591f99f
# Parent  c007e6d9941df278c5cd4b1588c1e5fdc46eedc6
tuned markup;

diff -r c007e6d9941d -r c92efbf32bfe src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Oct 01 20:39:16 2024 +0200
+++ b/src/HOL/HOL.thy	Tue Oct 01 21:30:59 2024 +0200
@@ -191,11 +191,11 @@
 nonterminal case_syn and cases_syn
 syntax
   "_case_syntax" :: "['a, cases_syn] \<Rightarrow> 'b"  (\<open>(\<open>notation=\<open>mixfix case expression\<close>\<close>case _ of/ _)\<close> 10)
-  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  (\<open>(\<open>indent=2 notation=\<open>mixfix case pattern\<close>\<close>_ \<Rightarrow>/ _)\<close> 10)
+  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  (\<open>(\<open>indent=2 notation=\<open>mixfix case clause\<close>\<close>_ \<Rightarrow>/ _)\<close> 10)
   "" :: "case_syn \<Rightarrow> cases_syn"  (\<open>_\<close>)
   "_case2" :: "[case_syn, cases_syn] \<Rightarrow> cases_syn"  (\<open>_/ | _\<close>)
 syntax (ASCII)
-  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  (\<open>(\<open>indent=2 notation=\<open>mixfix case pattern\<close>\<close>_ =>/ _)\<close> 10)
+  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  (\<open>(\<open>indent=2 notation=\<open>mixfix case clause\<close>\<close>_ =>/ _)\<close> 10)
 
 notation (ASCII)
   All  (binder \<open>ALL \<close> 10) and