Rephrease intro

leanprover · Feb 26, 2024 · ec87eb1 · ec87eb1
1 parent cbaad44
commit ec87eb1
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
@@ -15,9 +15,10 @@ import Lean.Elab.PreDefinition.WF.PackMutual
 import Lean.Elab.Command
 
 /-!
-This module contains code to derive, from the definition of a (possibly mutual) well-founded
-recursive function, a **functional induction principle** tailored to proofs about that
-function. For example from:
+This module contains code to derive, from the definition of a recursive function
+(or mutually recursive functions) defined by well-founded recursion, a
+**functional induction principle** tailored to proofs about that function(s). For
+example from:
 
 ```
 def ackermann : Nat → Nat → Nat