equal
deleted
inserted
replaced
17 val proof_of: bool -> thm -> Proofterm.proof |
17 val proof_of: bool -> thm -> Proofterm.proof |
18 val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T |
18 val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T |
19 val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T |
19 val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T |
20 end; |
20 end; |
21 |
21 |
22 structure ProofSyntax : PROOF_SYNTAX = |
22 structure Proof_Syntax : PROOF_SYNTAX = |
23 struct |
23 struct |
24 |
24 |
25 open Proofterm; |
25 open Proofterm; |
26 |
26 |
27 (**** add special syntax for embedding proof terms ****) |
27 (**** add special syntax for embedding proof terms ****) |