changeset 70840 | 5b80eb4fd0f3 |
parent 70493 | a9053fa30909 |
child 70847 | e62d5433bb47 |
--- a/src/HOL/Tools/rewrite_hol_proof.ML Fri Oct 11 21:51:10 2019 +0200 +++ b/src/HOL/Tools/rewrite_hol_proof.ML Fri Oct 11 22:01:45 2019 +0200 @@ -10,7 +10,7 @@ val elim_cong: typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option end; -structure RewriteHOLProof : REWRITE_HOL_PROOF = +structure Rewrite_HOL_Proof : REWRITE_HOL_PROOF = struct val rews =