Start using the ‖-notation also in its translation

jeltsch · jeltsch · commit d8c1ea60c360 · 2023-05-18T21:54:05.000+03:00
diff --git a/src/Thorn_Calculus-Processes.thy b/src/Thorn_Calculus-Processes.thy
@@ -63,7 +63,7 @@ syntax
   "_general_parallel" :: "pttrn \<Rightarrow> 'a list \<Rightarrow> 'p \<Rightarrow> 'p"
   (\<open>(3\<Parallel>_ \<leftarrow> _. _)\<close> [0, 0, 52] 52)
 translations
-  "_general_parallel v vs p" \<rightleftharpoons> "CONST general_parallel (\<lambda>v. p) vs"
+  "\<Parallel>v \<leftarrow> vs. p" \<rightleftharpoons> "CONST general_parallel (\<lambda>v. p) vs"
 print_translation \<open>
   [
     preserve_binder_abs_general_parallel_tr'

Original file line number	Diff line number	Diff line change
`@@ -63,7 +63,7 @@ syntax`
`63`	`63`	`"_general_parallel" :: "pttrn \<Rightarrow> 'a list \<Rightarrow> 'p \<Rightarrow> 'p"`
`64`	`64`	`(\<open>(3\<Parallel>_ \<leftarrow> _. _)\<close> [0, 0, 52] 52)`
`65`	`65`	`translations`
`66`		`- "_general_parallel v vs p" \<rightleftharpoons> "CONST general_parallel (\<lambda>v. p) vs"`
	`66`	`+ "\<Parallel>v \<leftarrow> vs. p" \<rightleftharpoons> "CONST general_parallel (\<lambda>v. p) vs"`
`67`	`67`	`print_translation \<open>`
`68`	`68`	`[`
`69`	`69`	`preserve_binder_abs_general_parallel_tr'`