equal
deleted
inserted
replaced
8 *) |
8 *) |
9 |
9 |
10 signature PROOF_REWRITE_RULES = |
10 signature PROOF_REWRITE_RULES = |
11 sig |
11 sig |
12 val rprocs : (string * (typ list -> Proofterm.proof -> Proofterm.proof option)) list |
12 val rprocs : (string * (typ list -> Proofterm.proof -> Proofterm.proof option)) list |
|
13 val setup : (theory -> theory) list |
13 end; |
14 end; |
14 |
15 |
15 structure ProofRewriteRules : PROOF_REWRITE_RULES = |
16 structure ProofRewriteRules : PROOF_REWRITE_RULES = |
16 struct |
17 struct |
17 |
18 |
109 (PAxm ("ProtoPure.reflexive", _, _) % _)) %% prf) = Some prf |
110 (PAxm ("ProtoPure.reflexive", _, _) % _)) %% prf) = Some prf |
110 |
111 |
111 | rew _ _ = None; |
112 | rew _ _ = None; |
112 |
113 |
113 val rprocs = [("Pure/meta_equality", rew)]; |
114 val rprocs = [("Pure/meta_equality", rew)]; |
|
115 val setup = [Proofterm.add_prf_rprocs rprocs]; |
114 |
116 |
115 end; |
117 end; |
116 |
|
117 Proofterm.add_prf_rprocs ProtoPure.thy ProofRewriteRules.rprocs; |
|