Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/IOA/meta_theory/RefCorrectness.thy
changeset 10835 f4745d77e620
parent 5976 44290b71a85f
child 12218 6597093b77e7 
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -20,15 +20,15 @@
 defs
 
 corresp_ex_def
-  "corresp_ex A f ex == (f (fst ex),(corresp_exC A f`(snd ex)) (fst ex))"
+  "corresp_ex A f ex == (f (fst ex),(corresp_exC A f$(snd ex)) (fst ex))"
 
 
 corresp_exC_def
-  "corresp_exC A f  == (fix`(LAM h ex. (%s. case ex of 
+  "corresp_exC A f  == (fix$(LAM h ex. (%s. case ex of 
       nil =>  nil
     | x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr)))
-                              @@ ((h`xs) (snd pr)))
-                        `x) )))"
+                              @@ ((h$xs) (snd pr)))
+                        $x) )))"
  
 is_fair_ref_map_def
   "is_fair_ref_map f C A ==
isabelle