--- 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";
--- 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