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/Integ/IntDef.thy
changeset 20217 25b068a99d2b
parent 20186 56207a6f4cc5
child 20254 58b71535ed00 
--- a/src/HOL/Integ/IntDef.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -387,7 +387,7 @@
 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
 proof -
   have "(\<lambda>(x,y). {x-y}) respects intrel"
-    by (simp add: congruent_def, arith) 
+    by (simp add: congruent_def, arith)
   thus ?thesis
     by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
 qed
isabelle