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/Cardinals/Order_Union.thy
changeset 58127 b7cab82f488e
parent 55027 a74ea6d75571
child 58889 5b7a9633cfa8 
--- a/src/HOL/Cardinals/Order_Union.thy	Mon Sep 01 16:34:38 2014 +0200
+++ b/src/HOL/Cardinals/Order_Union.thy	Mon Sep 01 16:34:39 2014 +0200
@@ -78,7 +78,7 @@
 assumes FLD: "Field r Int Field r' = {}" and
         REFL: "Refl r" and REFL': "Refl r'"
 shows "Refl (r Osum r')"
-using assms 
+using assms
 unfolding refl_on_def Field_Osum unfolding Osum_def by blast
 
 lemma Osum_trans:
isabelle