--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Fri Jul 12 22:41:25 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Sat Jul 13 12:38:40 2013 +0200
@@ -2,8 +2,8 @@
Author: Jasmin Blanchette, TU Muenchen
Author: Steffen Juilf Smolka, TU Muenchen
-Compression of isar proofs.
-Only proof steps using the MetisM proof_method are compressed.
+Compression of isar proofs by merging steps.
+Only proof steps using the MetisM proof_method are merged.
PRE CONDITION: the proof must be labeled canocially, see
Slegehammer_Proof.relabel_proof_canonically