equal
deleted
inserted
replaced
13 structure RewriteHOLProof : REWRITE_HOL_PROOF = |
13 structure RewriteHOLProof : REWRITE_HOL_PROOF = |
14 struct |
14 struct |
15 |
15 |
16 open Proofterm; |
16 open Proofterm; |
17 |
17 |
18 val rews = map (pairself (ProofSyntax.proof_of_term (the_context ()) true) o |
18 val rews = map (pairself (ProofSyntax.proof_of_term @{theory} true) o |
19 Logic.dest_equals o Logic.varify o ProofSyntax.read_term (the_context ()) propT) |
19 Logic.dest_equals o Logic.varify o ProofSyntax.read_term @{theory} propT) |
20 |
20 |
21 (** eliminate meta-equality rules **) |
21 (** eliminate meta-equality rules **) |
22 |
22 |
23 ["(equal_elim % x1 % x2 %% \ |
23 ["(equal_elim % x1 % x2 %% \ |
24 \ (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %% \ |
24 \ (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %% \ |