--- a/NEWS Tue Oct 08 16:15:31 2024 +0200
+++ b/NEWS Tue Oct 08 17:26:31 2024 +0200
@@ -65,7 +65,8 @@
notably like this:
unbundle no list_syntax
- unbundle no listcompr_syntax
+ unbundle no list_enumeration_syntax
+ unbundle no list_comprehension_syntax
unbundle no rtrancl_syntax
unbundle no trancl_syntax
unbundle no reflcl_syntax
--- a/src/Doc/Datatypes/Datatypes.thy Tue Oct 08 16:15:31 2024 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Oct 08 17:26:31 2024 +0200
@@ -360,8 +360,7 @@
"[x, xs]" == "x # [xs]"
"[x]" == "x # []"
- no_notation Nil (\<open>[]\<close>) and Cons (infixr \<open>#\<close> 65)
-
+ unbundle no list_syntax
hide_type list
hide_const Nil Cons case_list hd tl set map list_all2 rec_list size_list list_all
@@ -451,7 +450,7 @@
Incidentally, this is how the traditional syntax can be set up:
\<close>
(*<*)
-unbundle no list_syntax
+unbundle no list_enumeration_syntax
(*>*)
syntax "_list" :: "args \<Rightarrow> 'a list" (\<open>[(_)]\<close>)
--- a/src/HOL/Induct/SList.thy Tue Oct 08 16:15:31 2024 +0200
+++ b/src/HOL/Induct/SList.thy Tue Oct 08 17:26:31 2024 +0200
@@ -83,7 +83,7 @@
no_translations
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
-no_notation Nil (\<open>[]\<close>) and Cons (infixr \<open>#\<close> 65)
+unbundle no list_syntax
definition
Nil :: "'a list" (\<open>[]\<close>) where
--- a/src/HOL/List.thy Tue Oct 08 16:15:31 2024 +0200
+++ b/src/HOL/List.thy Tue Oct 08 17:26:31 2024 +0200
@@ -18,6 +18,12 @@
where
"tl [] = []"
+bundle list_syntax
+begin
+notation Nil (\<open>[]\<close>)
+ and Cons (infixr \<open>#\<close> 65)
+end
+
datatype_compat list
lemma [case_names Nil Cons, cases type: list]:
@@ -45,17 +51,14 @@
text \<open>List enumeration\<close>
-syntax
- "_list" :: "args \<Rightarrow> 'a list" (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
-translations
- "[x, xs]" \<rightleftharpoons> "x#[xs]"
- "[x]" \<rightleftharpoons> "x#[]"
-
-bundle list_syntax
+open_bundle list_enumeration_syntax
begin
syntax
"_list" :: "args \<Rightarrow> 'a list" (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
end
+translations
+ "[x, xs]" \<rightleftharpoons> "x#[xs]"
+ "[x]" \<rightleftharpoons> "x#[]"
subsection \<open>Basic list processing functions\<close>
@@ -447,6 +450,8 @@
nonterminal lc_qual and lc_quals
+open_bundle list_comprehension_syntax
+begin
syntax
"_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" (\<open>[_ . __\<close>)
"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" (\<open>_ \<leftarrow> _\<close>)
@@ -457,12 +462,6 @@
syntax (ASCII)
"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" (\<open>_ <- _\<close>)
-
-bundle listcompr_syntax
-begin
-syntax
- "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" (\<open>[_ . __\<close>)
- "_lc_end" :: "lc_quals" (\<open>]\<close>)
end
parse_translation \<open>