# HG changeset patch
# User wenzelm
# Date 1451509784 -3600
# Node ID 8c6226d88ced36a833bd9dca71ccd5484168536c
# Parent  ba465fcd02674f1d83c7b4c07b676a487103827a
more symbols;

diff -r ba465fcd0267 -r 8c6226d88ced src/HOL/HOLCF/IOA/ex/TrivEx.thy
--- 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)
diff -r ba465fcd0267 -r 8c6226d88ced src/HOL/HOLCF/IOA/ex/TrivEx2.thy
--- 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)
diff -r ba465fcd0267 -r 8c6226d88ced src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy
--- 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
diff -r ba465fcd0267 -r 8c6226d88ced src/HOL/HOLCF/IOA/meta_theory/TL.thy
--- 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)