equal
deleted
inserted
replaced
14 struct |
14 struct |
15 |
15 |
16 open Proofterm; |
16 open Proofterm; |
17 |
17 |
18 val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o |
18 val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o |
19 Logic.dest_equals o Logic.varify o Proof_Syntax.read_term @{theory} propT) |
19 Logic.dest_equals o Logic.varify_global o Proof_Syntax.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 %% \ |