author | wenzelm |
Fri, 26 Sep 2008 19:07:56 +0200 | |
changeset 28375 | c879d88d038a |
parent 27260 | 17d617c6b026 |
child 28807 | 9f3ecb4aaac2 |
permissions | -rw-r--r-- |
11522 | 1 |
(* Title: Pure/Proof/proof_syntax.ML |
2 |
ID: $Id$ |
|
11539 | 3 |
Author: Stefan Berghofer, TU Muenchen |
11522 | 4 |
|
5 |
Function for parsing and printing proof terms. |
|
6 |
*) |
|
7 |
||
8 |
signature PROOF_SYNTAX = |
|
9 |
sig |
|
17078 | 10 |
val proofT: typ |
11 |
val add_proof_syntax: theory -> theory |
|
12 |
val disambiguate_names: theory -> Proofterm.proof -> |
|
11522 | 13 |
Proofterm.proof * Proofterm.proof Symtab.table |
17078 | 14 |
val proof_of_term: theory -> Proofterm.proof Symtab.table -> |
11522 | 15 |
bool -> term -> Proofterm.proof |
17078 | 16 |
val term_of_proof: Proofterm.proof -> term |
17 |
val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof) |
|
18 |
val read_term: theory -> typ -> string -> term |
|
19 |
val read_proof: theory -> bool -> string -> Proofterm.proof |
|
20 |
val proof_syntax: Proofterm.proof -> theory -> theory |
|
21 |
val proof_of: bool -> thm -> Proofterm.proof |
|
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
22 |
val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
23 |
val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T |
11522 | 24 |
end; |
25 |
||
26 |
structure ProofSyntax : PROOF_SYNTAX = |
|
27 |
struct |
|
28 |
||
29 |
open Proofterm; |
|
30 |
||
31 |
(**** add special syntax for embedding proof terms ****) |
|
32 |
||
33 |
val proofT = Type ("proof", []); |
|
11614 | 34 |
val paramT = Type ("param", []); |
35 |
val paramsT = Type ("params", []); |
|
11522 | 36 |
val idtT = Type ("idt", []); |
24848 | 37 |
val aT = TFree (Name.aT, []); |
11522 | 38 |
|
39 |
(** constants for theorems and axioms **) |
|
40 |
||
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
41 |
fun add_proof_atom_consts names thy = |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
42 |
thy |
22796 | 43 |
|> Sign.absolute_path |
44 |
|> Sign.add_consts_i (map (fn name => (name, proofT, NoSyn)) names); |
|
11522 | 45 |
|
46 |
(** constants for application and abstraction **) |
|
11614 | 47 |
|
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
48 |
fun add_proof_syntax thy = |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
49 |
thy |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
50 |
|> Theory.copy |
22796 | 51 |
|> Sign.root_path |
52 |
|> Sign.add_defsort_i [] |
|
53 |
|> Sign.add_types [("proof", 0, NoSyn)] |
|
54 |
|> Sign.add_consts_i |
|
11614 | 55 |
[("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)), |
56 |
("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)), |
|
11522 | 57 |
("Abst", (aT --> proofT) --> proofT, NoSyn), |
13199 | 58 |
("AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn), |
59 |
("Hyp", propT --> proofT, NoSyn), |
|
60 |
("Oracle", propT --> proofT, NoSyn), |
|
61 |
("MinProof", proofT, Delimfix "?")] |
|
22796 | 62 |
|> Sign.add_nonterminals ["param", "params"] |
63 |
|> Sign.add_syntax_i |
|
11640 | 64 |
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)), |
11614 | 65 |
("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)), |
66 |
("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)), |
|
67 |
("_Lam1", [idtT, propT] ---> paramT, Mixfix ("_: _", [0, 0], 0)), |
|
68 |
("", paramT --> paramT, Delimfix "'(_')"), |
|
69 |
("", idtT --> paramsT, Delimfix "_"), |
|
70 |
("", paramT --> paramsT, Delimfix "_")] |
|
22796 | 71 |
|> Sign.add_modesyntax_i ("xsymbols", true) |
11640 | 72 |
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<Lambda>_./ _)", [0, 3], 3)), |
11522 | 73 |
("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)), |
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
74 |
("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))] |
22796 | 75 |
|> Sign.add_modesyntax_i ("latex", false) |
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
76 |
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))] |
22796 | 77 |
|> Sign.add_trrules_i (map Syntax.ParsePrintRule |
11522 | 78 |
[(Syntax.mk_appl (Constant "_Lam") |
11614 | 79 |
[Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"], |
80 |
Syntax.mk_appl (Constant "_Lam") |
|
81 |
[Variable "l", Syntax.mk_appl (Constant "_Lam") [Variable "m", Variable "A"]]), |
|
82 |
(Syntax.mk_appl (Constant "_Lam") |
|
11522 | 83 |
[Syntax.mk_appl (Constant "_Lam1") [Variable "x", Variable "A"], Variable "B"], |
84 |
Syntax.mk_appl (Constant "AbsP") [Variable "A", |
|
85 |
(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "B"])]), |
|
11614 | 86 |
(Syntax.mk_appl (Constant "_Lam") [Variable "x", Variable "A"], |
11522 | 87 |
Syntax.mk_appl (Constant "Abst") |
11614 | 88 |
[(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])])]); |
11522 | 89 |
|
90 |
||
91 |
(**** create unambiguous theorem names ****) |
|
92 |
||
93 |
fun disambiguate_names thy prf = |
|
94 |
let |
|
17019
f68598628d08
Adapted to new interface og thms_of_proof / axms_of_proof.
berghofe
parents:
16866
diff
changeset
|
95 |
val thms = thms_of_proof prf Symtab.empty; |
16866 | 96 |
val thms' = map (apsnd Thm.full_prop_of) (PureThy.all_thms_of thy); |
11522 | 97 |
|
21056 | 98 |
val tab = Symtab.fold (fn (key, ps) => fn tab => |
19473 | 99 |
let val prop = the_default (Bound 0) (AList.lookup (op =) thms' key) |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
100 |
in fst (fold_rev (fn (prop', prf) => fn x as (tab, i) => |
11522 | 101 |
if prop <> prop' then |
17412 | 102 |
(Symtab.update (key ^ "_" ^ string_of_int i, prf) tab, i+1) |
21056 | 103 |
else x) ps (tab, 1)) |
104 |
end) thms Symtab.empty; |
|
11522 | 105 |
|
106 |
fun rename (Abst (s, T, prf)) = Abst (s, T, rename prf) |
|
107 |
| rename (AbsP (s, t, prf)) = AbsP (s, t, rename prf) |
|
11614 | 108 |
| rename (prf1 %% prf2) = rename prf1 %% rename prf2 |
109 |
| rename (prf % t) = rename prf % t |
|
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21056
diff
changeset
|
110 |
| rename (prf' as PThm (s, prf, prop, Ts)) = |
11522 | 111 |
let |
19473 | 112 |
val prop' = the_default (Bound 0) (AList.lookup (op =) thms' s); |
19305 | 113 |
val ps = remove (op =) prop' (map fst (the (Symtab.lookup thms s))) |
11522 | 114 |
in if prop = prop' then prf' else |
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21056
diff
changeset
|
115 |
PThm (s ^ "_" ^ string_of_int (length ps - find_index (fn p => p = prop) ps), |
11522 | 116 |
prf, prop, Ts) |
117 |
end |
|
118 |
| rename prf = prf |
|
119 |
||
120 |
in (rename prf, tab) end; |
|
121 |
||
122 |
||
123 |
(**** translation between proof terms and pure terms ****) |
|
124 |
||
125 |
fun proof_of_term thy tab ty = |
|
126 |
let |
|
16350 | 127 |
val thms = PureThy.all_thms_of thy; |
128 |
val axms = Theory.all_axioms_of thy; |
|
11522 | 129 |
|
20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
19618
diff
changeset
|
130 |
fun mk_term t = (if ty then I else map_types (K dummyT)) |
11614 | 131 |
(Term.no_dummy_patterns t); |
132 |
||
11522 | 133 |
fun prf_of [] (Bound i) = PBound i |
134 |
| prf_of Ts (Const (s, Type ("proof", _))) = |
|
15531 | 135 |
change_type (if ty then SOME Ts else NONE) |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21646
diff
changeset
|
136 |
(case NameSpace.explode s of |
11614 | 137 |
"axm" :: xs => |
11522 | 138 |
let |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21646
diff
changeset
|
139 |
val name = NameSpace.implode xs; |
17223 | 140 |
val prop = (case AList.lookup (op =) axms name of |
15531 | 141 |
SOME prop => prop |
142 |
| NONE => error ("Unknown axiom " ^ quote name)) |
|
143 |
in PAxm (name, prop, NONE) end |
|
11614 | 144 |
| "thm" :: xs => |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21646
diff
changeset
|
145 |
let val name = NameSpace.implode xs; |
17223 | 146 |
in (case AList.lookup (op =) thms name of |
15531 | 147 |
SOME thm => fst (strip_combt (Thm.proof_of thm)) |
17412 | 148 |
| NONE => (case Symtab.lookup tab name of |
15531 | 149 |
SOME prf => prf |
150 |
| NONE => error ("Unknown theorem " ^ quote name))) |
|
11522 | 151 |
end |
152 |
| _ => error ("Illegal proof constant name: " ^ quote s)) |
|
13199 | 153 |
| prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop |
11522 | 154 |
| prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v |
155 |
| prf_of [] (Const ("Abst", _) $ Abs (s, T, prf)) = |
|
25245
1fcfcdcba53c
Added well-formedness check to Abst case in function prf_of.
berghofe
parents:
24848
diff
changeset
|
156 |
if T = proofT then |
1fcfcdcba53c
Added well-formedness check to Abst case in function prf_of.
berghofe
parents:
24848
diff
changeset
|
157 |
error ("Term variable abstraction may not bind proof variable " ^ quote s) |
1fcfcdcba53c
Added well-formedness check to Abst case in function prf_of.
berghofe
parents:
24848
diff
changeset
|
158 |
else Abst (s, if ty then SOME T else NONE, |
11522 | 159 |
incr_pboundvars (~1) 0 (prf_of [] prf)) |
160 |
| prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) = |
|
11614 | 161 |
AbsP (s, case t of |
15531 | 162 |
Const ("dummy_pattern", _) => NONE |
163 |
| _ $ Const ("dummy_pattern", _) => NONE |
|
164 |
| _ => SOME (mk_term t), |
|
11522 | 165 |
incr_pboundvars 0 (~1) (prf_of [] prf)) |
166 |
| prf_of [] (Const ("AppP", _) $ prf1 $ prf2) = |
|
11614 | 167 |
prf_of [] prf1 %% prf_of [] prf2 |
11522 | 168 |
| prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) = |
169 |
prf_of (T::Ts) prf |
|
11614 | 170 |
| prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf % |
15531 | 171 |
(case t of Const ("dummy_pattern", _) => NONE | _ => SOME (mk_term t)) |
11522 | 172 |
| prf_of _ t = error ("Not a proof term:\n" ^ |
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26626
diff
changeset
|
173 |
Syntax.string_of_term_global thy t) |
11522 | 174 |
|
175 |
in prf_of [] end; |
|
176 |
||
177 |
||
178 |
val AbsPt = Const ("AbsP", [propT, proofT --> proofT] ---> proofT); |
|
179 |
val AppPt = Const ("AppP", [proofT, proofT] ---> proofT); |
|
13199 | 180 |
val Hypt = Const ("Hyp", propT --> proofT); |
181 |
val Oraclet = Const ("Oracle", propT --> proofT); |
|
182 |
val MinProoft = Const ("MinProof", proofT); |
|
11522 | 183 |
|
19473 | 184 |
val mk_tyapp = fold (fn T => fn prf => Const ("Appt", |
19391 | 185 |
[proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T); |
11522 | 186 |
|
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21056
diff
changeset
|
187 |
fun term_of _ (PThm (name, _, _, NONE)) = |
16195 | 188 |
Const (NameSpace.append "thm" name, proofT) |
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21056
diff
changeset
|
189 |
| term_of _ (PThm (name, _, _, SOME Ts)) = |
19473 | 190 |
mk_tyapp Ts (Const (NameSpace.append "thm" name, proofT)) |
16195 | 191 |
| term_of _ (PAxm (name, _, NONE)) = Const (NameSpace.append "axm" name, proofT) |
15531 | 192 |
| term_of _ (PAxm (name, _, SOME Ts)) = |
19473 | 193 |
mk_tyapp Ts (Const (NameSpace.append "axm" name, proofT)) |
11522 | 194 |
| term_of _ (PBound i) = Bound i |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
195 |
| term_of Ts (Abst (s, opT, prf)) = |
18939 | 196 |
let val T = the_default dummyT opT |
11522 | 197 |
in Const ("Abst", (T --> proofT) --> proofT) $ |
198 |
Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf)) |
|
199 |
end |
|
200 |
| term_of Ts (AbsP (s, t, prf)) = |
|
18939 | 201 |
AbsPt $ the_default (Term.dummy_pattern propT) t $ |
11522 | 202 |
Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf)) |
11614 | 203 |
| term_of Ts (prf1 %% prf2) = |
11522 | 204 |
AppPt $ term_of Ts prf1 $ term_of Ts prf2 |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
205 |
| term_of Ts (prf % opt) = |
18939 | 206 |
let val t = the_default (Term.dummy_pattern dummyT) opt |
11522 | 207 |
in Const ("Appt", |
208 |
[proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $ |
|
209 |
term_of Ts prf $ t |
|
210 |
end |
|
211 |
| term_of Ts (Hyp t) = Hypt $ t |
|
212 |
| term_of Ts (Oracle (_, t, _)) = Oraclet $ t |
|
213 |
| term_of Ts (MinProof _) = MinProoft; |
|
214 |
||
215 |
val term_of_proof = term_of []; |
|
216 |
||
217 |
fun cterm_of_proof thy prf = |
|
218 |
let |
|
219 |
val (prf', tab) = disambiguate_names thy prf; |
|
28375 | 220 |
val thm_names = filter_out (fn s => s = "") |
16350 | 221 |
(map fst (PureThy.all_thms_of thy) @ map fst (Symtab.dest tab)); |
222 |
val axm_names = map fst (Theory.all_axioms_of thy); |
|
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
223 |
val thy' = thy |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
224 |
|> add_proof_syntax |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
225 |
|> add_proof_atom_consts |
16195 | 226 |
(map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names) |
11522 | 227 |
in |
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
228 |
(cterm_of thy' (term_of_proof prf'), |
11522 | 229 |
proof_of_term thy tab true o Thm.term_of) |
230 |
end; |
|
231 |
||
232 |
fun read_term thy = |
|
233 |
let |
|
28375 | 234 |
val thm_names = filter_out (fn s => s = "") (map fst (PureThy.all_thms_of thy)); |
16350 | 235 |
val axm_names = map fst (Theory.all_axioms_of thy); |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
236 |
val ctxt = thy |
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
237 |
|> add_proof_syntax |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16350
diff
changeset
|
238 |
|> add_proof_atom_consts |
16195 | 239 |
(map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names) |
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
240 |
|> ProofContext.init |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
241 |
|> ProofContext.allow_dummies |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
242 |
|> ProofContext.set_mode ProofContext.mode_schematic; |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
243 |
in |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
244 |
fn ty => fn s => |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
245 |
(if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
246 |
|> TypeInfer.constrain ty |> Syntax.check_term ctxt |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
247 |
end; |
11522 | 248 |
|
249 |
fun read_proof thy = |
|
250 |
let val rd = read_term thy proofT |
|
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
251 |
in fn ty => fn s => proof_of_term thy Symtab.empty ty (Logic.varify (rd s)) end; |
11522 | 252 |
|
17078 | 253 |
fun proof_syntax prf = |
11522 | 254 |
let |
28375 | 255 |
val thm_names = filter_out (fn s => s = "") |
19305 | 256 |
(map fst (Symtab.dest (thms_of_proof prf Symtab.empty))); |
17019
f68598628d08
Adapted to new interface og thms_of_proof / axms_of_proof.
berghofe
parents:
16866
diff
changeset
|
257 |
val axm_names = map fst (Symtab.dest (axms_of_proof prf Symtab.empty)); |
11522 | 258 |
in |
17078 | 259 |
add_proof_syntax #> |
260 |
add_proof_atom_consts |
|
261 |
(map (NameSpace.append "thm") thm_names @ map (NameSpace.append "axm") axm_names) |
|
11522 | 262 |
end; |
263 |
||
17078 | 264 |
fun proof_of full thm = |
265 |
let |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25245
diff
changeset
|
266 |
val thy = Thm.theory_of_thm thm; |
17078 | 267 |
val prop = Thm.full_prop_of thm; |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25245
diff
changeset
|
268 |
val prf = Thm.proof_of thm; |
17078 | 269 |
val prf' = (case strip_combt (fst (strip_combP prf)) of |
270 |
(PThm (_, prf', prop', _), _) => if prop = prop' then prf' else prf |
|
271 |
| _ => prf) |
|
272 |
in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end; |
|
273 |
||
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
274 |
fun pretty_proof ctxt prf = |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
275 |
ProofContext.pretty_term_abbrev |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
276 |
(ProofContext.transfer_syntax (proof_syntax prf (ProofContext.theory_of ctxt)) ctxt) |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
277 |
(term_of_proof prf); |
17078 | 278 |
|
27260
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
279 |
fun pretty_proof_of ctxt full th = |
17d617c6b026
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm
parents:
26939
diff
changeset
|
280 |
pretty_proof ctxt (proof_of full th); |
11522 | 281 |
|
282 |
end; |