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/UNITY/Guar.thy
changeset 69313 b021008c5397
parent 67613 ce654b0e6d69 
--- a/src/HOL/UNITY/Guar.thy	Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/UNITY/Guar.thy	Sun Nov 18 18:07:51 2018 +0000
@@ -215,7 +215,7 @@
 by (simp add: guarantees_Int_right)
 
 lemma guarantees_INT_right_iff:
-     "(F \<in> X guarantees (INTER I Y)) = (\<forall>i\<in>I. F \<in> X guarantees (Y i))"
+     "(F \<in> X guarantees (\<Inter>(Y ` I))) = (\<forall>i\<in>I. F \<in> X guarantees (Y i))"
 by (simp add: guarantees_INT_right)
 
 lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X \<union> Y))"
@@ -276,7 +276,7 @@
 
 lemma guarantees_JN_INT: 
      "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i;  OK I F |]  
-      ==> (JOIN I F) \<in> (INTER I X) guarantees (INTER I Y)"
+      ==> (JOIN I F) \<in> (\<Inter>(X ` I)) guarantees (\<Inter>(Y ` I))"
 apply (unfold guar_def, auto)
 apply (drule bspec, assumption)
 apply (rename_tac "i")
@@ -287,7 +287,7 @@
 
 lemma guarantees_JN_UN: 
     "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i;  OK I F |]  
-     ==> (JOIN I F) \<in> (UNION I X) guarantees (UNION I Y)"
+     ==> (JOIN I F) \<in> (\<Union>(X ` I)) guarantees (\<Union>(Y ` I))"
 apply (unfold guar_def, auto)
 apply (drule bspec, assumption)
 apply (rename_tac "i")
isabelle