# HG changeset patch # User smolkas # Date 1373711920 -7200 # Node ID 21774f0b7bc086280fb599fc3aa46a904be230bf # Parent 23393c31c7feebaae9ca358fa32818ac60548e4a tuned diff -r 23393c31c7fe -r 21774f0b7bc0 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML --- 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 diff -r 23393c31c7fe -r 21774f0b7bc0 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Jul 12 22:41:25 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Sat Jul 13 12:38:40 2013 +0200 @@ -115,7 +115,7 @@ |> thm_of_term ctxt end -(* mapping of proof methods to tactics *) +(* mapping from proof methods to tactics *) fun tac_of_method method type_enc lam_trans ctxt facts = case method of MetisM => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts @@ -123,7 +123,7 @@ Method.insert_tac facts THEN' (case method of SimpM => Simplifier.asm_full_simp_tac - | AutoM => (fn ctxt => K (Clasimp.auto_tac ctxt)) + | AutoM => Clasimp.auto_tac #> K | FastforceM => Clasimp.fast_force_tac | ForceM => Clasimp.force_tac | ArithM => Arith_Data.arith_tac