# HG changeset patch # User smolkas # Date 1373542399 -7200 # Node ID 02713cd2c2cd32840b49c822bd72e193b7bdd813 # Parent d28d2d89034d46ad15080ed61b61305143e28500 tuned diff -r d28d2d89034d -r 02713cd2c2cd src/HOL/Tools/Sledgehammer/sledgehammer_print.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Thu Jul 11 11:40:21 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Thu Jul 11 13:33:19 2013 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML +(* Title: HOL/Tools/Sledgehammer/sledgehammer_print.ML Author: Jasmin Blanchette, TU Muenchen Author: Steffen Juilf Smolka, TU Muenchen diff -r d28d2d89034d -r 02713cd2c2cd src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Thu Jul 11 11:40:21 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Thu Jul 11 13:33:19 2013 +0200 @@ -20,8 +20,8 @@ Proof of fix * assms * isar_step list and isar_step = Let of term * term | - (* for |fix|>0, this is an obtain step; step may contain subproofs *) - Prove of isar_qualifier list * fix * label * term * isar_proof list * byline + (* for |fix|>0, this is an obtain step; step may contain subproofs *) + Prove of isar_qualifier list * fix * label * term * isar_proof list * byline and byline = By_Metis of facts diff -r d28d2d89034d -r 02713cd2c2cd src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Thu Jul 11 11:40:21 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Thu Jul 11 13:33:19 2013 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML +(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Author: Jasmin Blanchette, TU Muenchen Author: Steffen Juilf Smolka, TU Muenchen