diff -r 93dce7c71929 -r d705d7ae2410 Quot/Examples/IntEx2.thy --- a/Quot/Examples/IntEx2.thy Fri Dec 11 19:19:50 2009 +0100 +++ b/Quot/Examples/IntEx2.thy Fri Dec 11 19:22:30 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])