# HG changeset patch
# User wenzelm
# Date 1573243174 -3600
# Node ID 3c04a52c422ad9f9743bcf26a398c57611dda445
# Parent  fd82d53c176132a7de0bf9f7baa9c091702412c8
tuned comments;

diff -r fd82d53c1761 -r 3c04a52c422a src/HOL/Tools/rewrite_hol_proof.ML
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Fri Nov 08 20:28:50 2019 +0100
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Fri Nov 08 20:59:34 2019 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Tools/rewrite_hol_proof.ML
     Author:     Stefan Berghofer, TU Muenchen
 
-Rewrite rules for HOL proofs
+Rewrite rules for HOL proofs.
 *)
 
 signature REWRITE_HOL_PROOF =