diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Simulations.thy
--- a/src/HOLCF/IOA/meta_theory/Simulations.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Simulations.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -23,7 +23,7 @@
 
 is_simulation_def
   "is_simulation R C A ==                          
-   (!s:starts_of C. R```{s} Int starts_of A ~= {}) &        
+   (!s:starts_of C. R``{s} Int starts_of A ~= {}) &        
    (!s s' t a. reachable C s &                      
                s -a--C-> t   &
                (s,s') : R              
@@ -31,7 +31,7 @@
 
 is_backward_simulation_def
   "is_backward_simulation R C A ==                          
-   (!s:starts_of C. R```{s} <= starts_of A) &        
+   (!s:starts_of C. R``{s} <= starts_of A) &        
    (!s t t' a. reachable C s &                      
                s -a--C-> t   &
                (t,t') : R