--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Mon Jun 09 10:21:38 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Thu Jun 12 16:47:15 1997 +0200
@@ -8,26 +8,26 @@
RefCorrectness = RefMappings +
-
+
consts
corresp_ex ::"('a,'s2)ioa => ('s1 => 's2) =>
('a,'s1)execution => ('a,'s2)execution"
- corresp_ex2 ::"('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs
- -> ('s2 => ('a,'s2)pairs)"
+ corresp_exC ::"('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs
+ -> ('s1 => ('a,'s2)pairs)"
defs
corresp_ex_def
- "corresp_ex A f ex == (f (fst ex),(corresp_ex2 A f`(snd ex)) (f (fst ex)))"
+ "corresp_ex A f ex == (f (fst ex),(corresp_exC A f`(snd ex)) (fst ex))"
-corresp_ex2_def
- "corresp_ex2 A f == (fix`(LAM h ex. (%s. case ex of
+corresp_exC_def
+ "corresp_exC A f == (fix`(LAM h ex. (%s. case ex of
nil => nil
- | x##xs => (flift1 (%pr. (snd(@cex. move A cex s (fst pr) (f (snd pr))))
- @@ ((h`xs) (f (snd pr))))
+ | x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr)))
+ @@ ((h`xs) (snd pr)))
`x) )))"