--- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy Wed Dec 30 22:05:00 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy Wed Dec 30 22:09:44 2015 +0100
@@ -45,7 +45,7 @@
"h_abs n = (n~=0)"
axiomatization where
- MC_result: "validIOA A_ioa (\<diamond>\<box><%(b,a,c). b>)"
+ MC_result: "validIOA A_ioa (\<diamond>\<box>\<langle>%(b,a,c). b\<rangle>)"
lemma h_abs_is_abstraction:
"is_abstraction h_abs C_ioa A_ioa"
@@ -61,7 +61,7 @@
apply (simp add: h_abs_def)
done
-lemma TrivEx_abstraction: "validIOA C_ioa (\<diamond>\<box><%(n,a,m). n~=0>)"
+lemma TrivEx_abstraction: "validIOA C_ioa (\<diamond>\<box>\<langle>%(n,a,m). n~=0\<rangle>)"
apply (rule AbsRuleT1)
apply (rule h_abs_is_abstraction)
apply (rule MC_result)
--- a/src/HOL/HOLCF/IOA/ex/TrivEx2.thy Wed Dec 30 22:05:00 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx2.thy Wed Dec 30 22:09:44 2015 +0100
@@ -51,7 +51,7 @@
"h_abs n = (n~=0)"
axiomatization where
- MC_result: "validLIOA (A_ioa,WF A_ioa {INC}) (\<diamond>\<box><%(b,a,c). b>)"
+ MC_result: "validLIOA (A_ioa,WF A_ioa {INC}) (\<diamond>\<box>\<langle>%(b,a,c). b\<rangle>)"
lemma h_abs_is_abstraction:
@@ -90,7 +90,7 @@
lemma TrivEx2_abstraction:
- "validLIOA C_live_ioa (\<diamond>\<box><%(n,a,m). n~=0>)"
+ "validLIOA C_live_ioa (\<diamond>\<box>\<langle>%(n,a,m). n~=0\<rangle>)"
apply (unfold C_live_ioa_def)
apply (rule AbsRuleT2)
apply (rule h_abs_is_liveabstraction)
--- a/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy Wed Dec 30 22:05:00 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy Wed Dec 30 22:09:44 2015 +0100
@@ -19,10 +19,10 @@
definition
WF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
- "WF A acts = (\<diamond>\<box><%(s,a,t) . Enabled A acts s> \<^bold>\<longrightarrow> \<box>\<diamond><xt2 (plift (%a. a : acts))>)"
+ "WF A acts = (\<diamond>\<box>\<langle>%(s,a,t). Enabled A acts s\<rangle> \<^bold>\<longrightarrow> \<box>\<diamond>\<langle>xt2 (plift (%a. a : acts))\<rangle>)"
definition
SF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
- "SF A acts = (\<box>\<diamond><%(s,a,t) . Enabled A acts s> \<^bold>\<longrightarrow> \<box>\<diamond><xt2 (plift (%a. a : acts))>)"
+ "SF A acts = (\<box>\<diamond>\<langle>%(s,a,t). Enabled A acts s\<rangle> \<^bold>\<longrightarrow> \<box>\<diamond>\<langle>xt2 (plift (%a. a : acts))\<rangle>)"
definition
liveexecutions :: "('a,'s)live_ioa => ('a,'s)execution set" where
--- a/src/HOL/HOLCF/IOA/meta_theory/TL.thy Wed Dec 30 22:05:00 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TL.thy Wed Dec 30 22:09:44 2015 +0100
@@ -22,7 +22,7 @@
unlift :: "'a lift => 'a"
-Init :: "'a predicate => 'a temporal" ("<_>" [0] 1000)
+Init :: "'a predicate => 'a temporal" ("\<langle>_\<rangle>" [0] 1000)
Box :: "'a temporal => 'a temporal" ("\<box>(_)" [80] 80)
Diamond :: "'a temporal => 'a temporal" ("\<diamond>(_)" [80] 80)