equal
deleted
inserted
replaced
8 sig |
8 sig |
9 val rews: (Proofterm.proof * Proofterm.proof) list |
9 val rews: (Proofterm.proof * Proofterm.proof) list |
10 val elim_cong: typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option |
10 val elim_cong: typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option |
11 end; |
11 end; |
12 |
12 |
13 structure RewriteHOLProof : REWRITE_HOL_PROOF = |
13 structure Rewrite_HOL_Proof : REWRITE_HOL_PROOF = |
14 struct |
14 struct |
15 |
15 |
16 val rews = |
16 val rews = |
17 map (apply2 (Proof_Syntax.proof_of_term \<^theory> true) o Logic.dest_equals o |
17 map (apply2 (Proof_Syntax.proof_of_term \<^theory> true) o Logic.dest_equals o |
18 Logic.varify_global o Proof_Syntax.read_term \<^theory> true propT o Syntax.implode_input) |
18 Logic.varify_global o Proof_Syntax.read_term \<^theory> true propT o Syntax.implode_input) |