equal
deleted
inserted
replaced
12 |
12 |
13 structure RewriteHOLProof : REWRITE_HOL_PROOF = |
13 structure RewriteHOLProof : 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) |
19 |
19 |
20 (** eliminate meta-equality rules **) |
20 (** eliminate meta-equality rules **) |
21 |
21 |
22 [\<open>(equal_elim \<cdot> x1 \<cdot> x2 \<bullet> |
22 [\<open>(equal_elim \<cdot> x1 \<cdot> x2 \<bullet> |
23 (combination \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> Trueprop \<cdot> x3 \<cdot> A \<cdot> B \<bullet> |
23 (combination \<cdot> TYPE('T1) \<cdot> TYPE('T2) \<cdot> Trueprop \<cdot> x3 \<cdot> A \<cdot> B \<bullet> |