--- a/src/HOL/Bali/AxSound.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Bali/AxSound.thy Fri Sep 20 19:51:08 2024 +0200
@@ -10,7 +10,7 @@
subsubsection "validity"
definition
- triple_valid2 :: "prog \<Rightarrow> nat \<Rightarrow> 'a triple \<Rightarrow> bool" ("_\<Turnstile>_\<Colon>_"[61,0, 58] 57)
+ triple_valid2 :: "prog \<Rightarrow> nat \<Rightarrow> 'a triple \<Rightarrow> bool" (\<open>_\<Turnstile>_\<Colon>_\<close>[61,0, 58] 57)
where
"G\<Turnstile>n\<Colon>t =
(case t of {P} t\<succ> {Q} \<Rightarrow>
@@ -28,7 +28,7 @@
\<close>
definition
- ax_valids2 :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<Turnstile>\<Colon>_" [61,58,58] 57)
+ ax_valids2 :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" (\<open>_,_|\<Turnstile>\<Colon>_\<close> [61,58,58] 57)
where "G,A|\<Turnstile>\<Colon>ts = (\<forall>n. (\<forall>t\<in>A. G\<Turnstile>n\<Colon>t) \<longrightarrow> (\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t))"
lemma triple_valid2_def2: "G\<Turnstile>n\<Colon>{P} t\<succ> {Q} =