# HG changeset patch
# User wenzelm
# Date 953030010 -3600
# Node ID 614f18139d47cd682965be98eb5c3b319b034edd
# Parent  dc44d6533f0f9992a64aff4502070b9cbe18711f
tuned comments;

diff -r dc44d6533f0f -r 614f18139d47 src/HOL/Tools/induct_method.ML
--- a/src/HOL/Tools/induct_method.ML	Tue Mar 14 11:33:14 2000 +0100
+++ b/src/HOL/Tools/induct_method.ML	Tue Mar 14 11:33:30 2000 +0100
@@ -185,7 +185,7 @@
         cases         - classical case split
         cases t       - datatype exhaustion
   <x:A> cases ...     - set elimination
-  ...   cases ... r   - explicit rule
+  ...   cases ... R   - explicit rule
 *)
 
 local
@@ -248,7 +248,7 @@
         induct         - mathematical induction
         induct x       - datatype induction
   <x:A> induct ...     - set induction
-  ...   induct ... r   - explicit rule
+  ...   induct ... R   - explicit rule
 *)
 
 local