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/Analysis/Tagged_Division.thy
changeset 66884 c2128ab11f61
parent 66827 c94531b5007d
child 67399 eab6ce8368fa 
--- a/src/HOL/Analysis/Tagged_Division.thy	Tue Oct 17 13:56:58 2017 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy	Thu Oct 19 17:16:01 2017 +0100
@@ -66,7 +66,7 @@
   shows "interior i \<subseteq> interior S"
 proof -
   have "box a b \<inter> cbox c d = {}"
-     using inter_interval_mixed_eq_empty[of c d a b] assms
+     using Int_interval_mixed_eq_empty[of c d a b] assms
      unfolding interior_cbox by auto
   moreover
   have "box a b \<subseteq> cbox c d \<union> S"
isabelle