Mercurial Mercurial > hg > nominal2 / 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.
Quot/Examples/IntEx2.thy
changeset 719 a9e55e1ef64c
parent 715 3d7a9d4d2bb6
child 766 df053507edba 
--- a/Quot/Examples/IntEx2.thy	Fri Dec 11 16:32:40 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Fri Dec 11 17:19:38 2009 +0100
@@ -194,8 +194,8 @@
    (simp)
 
 lemma add:
-     "(ABS_int (x,y)) + (ABS_int (u,v)) =
-      (ABS_int (x + u, y + v))"
+     "(abs_int (x,y)) + (abs_int (u,v)) =
+      (abs_int (x + u, y + v))"
 apply(simp add: plus_int_def)
 apply(fold plus_raw.simps)
 apply(rule Quotient_rel_abs[OF Quotient_int])
nominal2