# HG changeset patch
# User nipkow
# Date 978716956 -3600
# Node ID 0a1446ff6aff303430b2326da520176413a76a10
# Parent  028d22926a4151ec6a49b76923ca8675ff56c92d
*** empty log message ***

diff -r 028d22926a41 -r 0a1446ff6aff src/HOLCF/IOA/meta_theory/Simulations.ML
--- a/src/HOLCF/IOA/meta_theory/Simulations.ML	Fri Jan 05 18:48:18 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Simulations.ML	Fri Jan 05 18:49:16 2001 +0100
@@ -19,7 +19,7 @@
 
 
 Goalw [Image_def]
-"(R^^{x} Int S ~= {}) = (? y. (x,y):R & y:S)";
+"(R```{x} Int S ~= {}) = (? y. (x,y):R & y:S)";
 by (simp_tac (simpset() addsimps [Int_non_empty]) 1);
 qed"Sim_start_convert";
 
diff -r 028d22926a41 -r 0a1446ff6aff src/HOLCF/IOA/meta_theory/Simulations.thy
--- a/src/HOLCF/IOA/meta_theory/Simulations.thy	Fri Jan 05 18:48:18 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Simulations.thy	Fri Jan 05 18:49:16 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