# HG changeset patch
# User wenzelm
# Date 1170622942 -3600
# Node ID 020f65c2cdabcdc160220dc9df3b2dec40838e1c
# Parent  5b2dc1b30e7aa449866bb3fd553f73d5c8ebfa14
removed non-modular comment;

diff -r 5b2dc1b30e7a -r 020f65c2cdab src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Sun Feb 04 22:02:21 2007 +0100
+++ b/src/HOL/Integ/IntArith.thy	Sun Feb 04 22:02:22 2007 +0100
@@ -173,7 +173,6 @@
 declare Zero_int_def [symmetric, simp]
 declare One_int_def [symmetric, simp]
 
-text{*cooper.ML refers to this theorem*}
 lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
 
 lemma nat_0: "nat 0 = 0"