# HG changeset patch
# User webertj
# Date 1258396392 0
# Node ID 474ebcc348e6c35a378afc8f2c602ac7038801d8
# Parent  06e9aff51d17eb5d9eaa39f3b3e813d73c1090c5
Fixed a typo in a comment.

diff -r 06e9aff51d17 -r 474ebcc348e6 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Mon Nov 16 17:22:10 2009 +0000
+++ b/src/HOL/Tools/lin_arith.ML	Mon Nov 16 18:33:12 2009 +0000
@@ -459,7 +459,7 @@
       in
         SOME [(HOLogic.natT :: Ts, subgoal1), (Ts, subgoal2)]
       end
-    (* "?P ((?n::nat) mod (number_of ?k)) =
+    (* ?P ((?n::nat) mod (number_of ?k)) =
          ((number_of ?k = 0 --> ?P ?n) & (~ (number_of ?k = 0) -->
            (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P j))) *)
     | (Const ("Divides.div_class.mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
@@ -491,7 +491,7 @@
       in
         SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
       end
-    (* "?P ((?n::nat) div (number_of ?k)) =
+    (* ?P ((?n::nat) div (number_of ?k)) =
          ((number_of ?k = 0 --> ?P 0) & (~ (number_of ?k = 0) -->
            (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P i))) *)
     | (Const ("Divides.div_class.div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
@@ -523,7 +523,7 @@
       in
         SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
       end
-    (* "?P ((?n::int) mod (number_of ?k)) =
+    (* ?P ((?n::int) mod (number_of ?k)) =
          ((iszero (number_of ?k) --> ?P ?n) &
           (neg (number_of (uminus ?k)) -->
             (ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
@@ -575,7 +575,7 @@
       in
         SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
       end
-    (* "?P ((?n::int) div (number_of ?k)) =
+    (* ?P ((?n::int) div (number_of ?k)) =
          ((iszero (number_of ?k) --> ?P 0) &
           (neg (number_of (uminus ?k)) -->
             (ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) --> ?P i)) &