src/HOL/HOLCF/IOA/meta_theory/TL.thy

 
 validT     :: "'a Seq predicate => bool"
 
 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)
 Next       :: "'a temporal => 'a temporal"
 Leadsto    :: "'a temporal => 'a temporal => 'a temporal"  (infixr "\<leadsto>" 22)