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/HOL/HOLCF/IOA/Simulations.thy
changeset 67613 ce654b0e6d69
parent 62192 bdaa0eb0fc74 
--- a/src/HOL/HOLCF/IOA/Simulations.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/HOLCF/IOA/Simulations.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -38,11 +38,11 @@
 
 definition is_history_relation :: "('s1 \<times> 's2) set \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
   where "is_history_relation R C A \<longleftrightarrow>
-    is_simulation R C A \<and> is_ref_map (\<lambda>x. (SOME y. (x, y) \<in> R^-1)) A C"
+    is_simulation R C A \<and> is_ref_map (\<lambda>x. (SOME y. (x, y) \<in> R\<inverse>)) A C"
 
 definition is_prophecy_relation :: "('s1 \<times> 's2) set \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
   where "is_prophecy_relation R C A \<longleftrightarrow>
-    is_backward_simulation R C A \<and> is_ref_map (\<lambda>x. (SOME y. (x, y) \<in> R^-1)) A C"
+    is_backward_simulation R C A \<and> is_ref_map (\<lambda>x. (SOME y. (x, y) \<in> R\<inverse>)) A C"
 
 
 lemma set_non_empty: "A \<noteq> {} \<longleftrightarrow> (\<exists>x. x \<in> A)"
isabelle