blanchet@56544
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
|
smolkas@51278
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
smolkas@51278
|
3 |
Author: Steffen Juilf Smolka, TU Muenchen
|
smolkas@51278
|
4 |
|
smolkas@51278
|
5 |
Basic data structures for representing and basic methods
|
smolkas@51278
|
6 |
for dealing with Isar proof texts.
|
smolkas@51278
|
7 |
*)
|
smolkas@51278
|
8 |
|
blanchet@56544
|
9 |
signature SLEDGEHAMMER_ISAR_PROOF =
|
smolkas@51274
|
10 |
sig
|
blanchet@56629
|
11 |
type proof_method = Sledgehammer_Proof_Methods.proof_method
|
blanchet@56627
|
12 |
|
wenzelm@52376
|
13 |
type label = string * int
|
blanchet@56158
|
14 |
type facts = label list * string list (* local and global facts *)
|
smolkas@51283
|
15 |
|
smolkas@52315
|
16 |
datatype isar_qualifier = Show | Then
|
smolkas@51283
|
17 |
|
smolkas@53591
|
18 |
datatype isar_proof =
|
blanchet@56042
|
19 |
Proof of (string * typ) list * (label * term) list * isar_step list
|
smolkas@52316
|
20 |
and isar_step =
|
smolkas@51283
|
21 |
Let of term * term |
|
blanchet@56622
|
22 |
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
|
blanchet@56641
|
23 |
* facts * proof_method list * string
|
smolkas@53729
|
24 |
|
smolkas@52316
|
25 |
val no_label : label
|
smolkas@51283
|
26 |
|
smolkas@53729
|
27 |
val label_ord : label * label -> order
|
blanchet@53135
|
28 |
val string_of_label : label -> string
|
smolkas@53729
|
29 |
|
blanchet@56602
|
30 |
val steps_of_isar_proof : isar_proof -> isar_step list
|
smolkas@52316
|
31 |
|
blanchet@56565
|
32 |
val label_of_isar_step : isar_step -> label option
|
blanchet@56621
|
33 |
val facts_of_isar_step : isar_step -> facts
|
blanchet@56621
|
34 |
val proof_methods_of_isar_step : isar_step -> proof_method list
|
smolkas@52316
|
35 |
|
blanchet@56107
|
36 |
val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
|
blanchet@56554
|
37 |
val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
|
blanchet@56554
|
38 |
val add_isar_steps : isar_step list -> int -> int
|
smolkas@53591
|
39 |
|
blanchet@56554
|
40 |
structure Canonical_Label_Tab : TABLE
|
smolkas@53693
|
41 |
|
smolkas@53693
|
42 |
val canonical_label_ord : (label * label) -> order
|
blanchet@56562
|
43 |
|
blanchet@56641
|
44 |
val comment_isar_proof : (label -> proof_method list -> string) -> isar_proof -> isar_proof
|
blanchet@56562
|
45 |
val chain_isar_proof : isar_proof -> isar_proof
|
blanchet@56562
|
46 |
val kill_useless_labels_in_isar_proof : isar_proof -> isar_proof
|
blanchet@56555
|
47 |
val relabel_isar_proof_canonically : isar_proof -> isar_proof
|
blanchet@56624
|
48 |
val relabel_isar_proof_nicely : isar_proof -> isar_proof
|
smolkas@53693
|
49 |
|
blanchet@56641
|
50 |
val string_of_isar_proof : Proof.context -> int -> int -> isar_proof -> string
|
blanchet@55877
|
51 |
end;
|
smolkas@51274
|
52 |
|
blanchet@56544
|
53 |
structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF =
|
smolkas@51274
|
54 |
struct
|
smolkas@51274
|
55 |
|
blanchet@56553
|
56 |
open ATP_Util
|
blanchet@56553
|
57 |
open ATP_Proof
|
blanchet@56553
|
58 |
open ATP_Problem_Generate
|
blanchet@56553
|
59 |
open ATP_Proof_Reconstruct
|
blanchet@56553
|
60 |
open Sledgehammer_Util
|
blanchet@56629
|
61 |
open Sledgehammer_Proof_Methods
|
blanchet@56553
|
62 |
open Sledgehammer_Isar_Annotate
|
blanchet@56553
|
63 |
|
smolkas@51274
|
64 |
type label = string * int
|
blanchet@55907
|
65 |
type facts = label list * string list (* local and global facts *)
|
smolkas@51274
|
66 |
|
smolkas@52315
|
67 |
datatype isar_qualifier = Show | Then
|
smolkas@51274
|
68 |
|
smolkas@53591
|
69 |
datatype isar_proof =
|
blanchet@56042
|
70 |
Proof of (string * typ) list * (label * term) list * isar_step list
|
smolkas@52316
|
71 |
and isar_step =
|
smolkas@51274
|
72 |
Let of term * term |
|
blanchet@56622
|
73 |
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
|
blanchet@56641
|
74 |
* facts * proof_method list * string
|
smolkas@53729
|
75 |
|
smolkas@52316
|
76 |
val no_label = ("", ~1)
|
smolkas@51274
|
77 |
|
smolkas@53729
|
78 |
val label_ord = pairself swap #> prod_ord int_ord fast_string_ord
|
smolkas@53693
|
79 |
|
blanchet@53135
|
80 |
fun string_of_label (s, num) = s ^ string_of_int num
|
smolkas@51274
|
81 |
|
blanchet@56602
|
82 |
fun steps_of_isar_proof (Proof (_, _, steps)) = steps
|
smolkas@52315
|
83 |
|
blanchet@56641
|
84 |
fun label_of_isar_step (Prove (_, _, l, _, _, _, _, _)) = SOME l
|
blanchet@56565
|
85 |
| label_of_isar_step _ = NONE
|
smolkas@52315
|
86 |
|
blanchet@56641
|
87 |
fun subproofs_of_isar_step (Prove (_, _, _, _, subs, _, _, _)) = subs
|
blanchet@56623
|
88 |
| subproofs_of_isar_step _ = []
|
smolkas@53591
|
89 |
|
blanchet@56641
|
90 |
fun facts_of_isar_step (Prove (_, _, _, _, _, facts, _, _)) = facts
|
blanchet@56621
|
91 |
| facts_of_isar_step _ = ([], [])
|
blanchet@56621
|
92 |
|
blanchet@56641
|
93 |
fun proof_methods_of_isar_step (Prove (_, _, _, _, _, _, meths, _)) = meths
|
blanchet@56621
|
94 |
| proof_methods_of_isar_step _ = []
|
smolkas@52316
|
95 |
|
blanchet@56554
|
96 |
fun fold_isar_step f step =
|
blanchet@56623
|
97 |
fold (steps_of_isar_proof #> fold_isar_steps f) (subproofs_of_isar_step step) #> f step
|
blanchet@56554
|
98 |
and fold_isar_steps f = fold (fold_isar_step f)
|
smolkas@53591
|
99 |
|
blanchet@56107
|
100 |
fun map_isar_steps f =
|
smolkas@53729
|
101 |
let
|
blanchet@56554
|
102 |
fun map_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map map_step steps)
|
blanchet@56554
|
103 |
and map_step (step as Let _) = f step
|
blanchet@56641
|
104 |
| map_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) =
|
blanchet@56641
|
105 |
f (Prove (qs, xs, l, t, map map_proof subs, facts, meths, comment))
|
blanchet@56554
|
106 |
in map_proof end
|
smolkas@53729
|
107 |
|
blanchet@56554
|
108 |
val add_isar_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I)
|
smolkas@53693
|
109 |
|
blanchet@56553
|
110 |
(* canonical proof labels: 1, 2, 3, ... in post traversal order *)
|
smolkas@53694
|
111 |
fun canonical_label_ord (((_, i1), (_, i2)) : label * label) = int_ord (i1, i2)
|
smolkas@53693
|
112 |
|
blanchet@56554
|
113 |
structure Canonical_Label_Tab = Table(
|
smolkas@53693
|
114 |
type key = label
|
smolkas@53693
|
115 |
val ord = canonical_label_ord)
|
smolkas@53693
|
116 |
|
blanchet@56641
|
117 |
fun comment_isar_step comment_of (Prove (qs, xs, l, t, subs, facts, meths, _)) =
|
blanchet@56641
|
118 |
Prove (qs, xs, l, t, subs, facts, meths, comment_of l meths)
|
blanchet@56641
|
119 |
| comment_isar_step _ step = step
|
blanchet@56641
|
120 |
fun comment_isar_proof comment_of = map_isar_steps (comment_isar_step comment_of)
|
blanchet@56641
|
121 |
|
blanchet@56562
|
122 |
fun chain_qs_lfs NONE lfs = ([], lfs)
|
blanchet@56562
|
123 |
| chain_qs_lfs (SOME l0) lfs =
|
blanchet@58997
|
124 |
if member (op =) lfs l0 then ([Then], remove (op =) l0 lfs) else ([], lfs)
|
blanchet@58997
|
125 |
|
blanchet@58628
|
126 |
fun chain_isar_step lbl (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) =
|
blanchet@56562
|
127 |
let val (qs', lfs) = chain_qs_lfs lbl lfs in
|
blanchet@56641
|
128 |
Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths, comment)
|
blanchet@56562
|
129 |
end
|
blanchet@56562
|
130 |
| chain_isar_step _ step = step
|
blanchet@56562
|
131 |
and chain_isar_steps _ [] = []
|
blanchet@58997
|
132 |
| chain_isar_steps prev (i :: is) =
|
blanchet@56565
|
133 |
chain_isar_step prev i :: chain_isar_steps (label_of_isar_step i) is
|
blanchet@56562
|
134 |
and chain_isar_proof (Proof (fix, assms, steps)) =
|
blanchet@56562
|
135 |
Proof (fix, assms, chain_isar_steps (try (List.last #> fst) assms) steps)
|
blanchet@56562
|
136 |
|
blanchet@56562
|
137 |
fun kill_useless_labels_in_isar_proof proof =
|
blanchet@56562
|
138 |
let
|
blanchet@56562
|
139 |
val used_ls =
|
blanchet@56621
|
140 |
fold_isar_steps (facts_of_isar_step #> fst #> union (op =)) (steps_of_isar_proof proof) []
|
blanchet@56562
|
141 |
|
blanchet@56562
|
142 |
fun kill_label l = if member (op =) used_ls l then l else no_label
|
blanchet@56562
|
143 |
|
blanchet@56641
|
144 |
fun kill_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) =
|
blanchet@56641
|
145 |
Prove (qs, xs, kill_label l, t, map kill_proof subs, facts, meths, comment)
|
blanchet@56562
|
146 |
| kill_step step = step
|
blanchet@56562
|
147 |
and kill_proof (Proof (fix, assms, steps)) =
|
blanchet@56562
|
148 |
Proof (fix, map (apfst kill_label) assms, map kill_step steps)
|
blanchet@56562
|
149 |
in
|
blanchet@56562
|
150 |
kill_proof proof
|
blanchet@56562
|
151 |
end
|
blanchet@56562
|
152 |
|
blanchet@56555
|
153 |
fun relabel_isar_proof_canonically proof =
|
smolkas@53693
|
154 |
let
|
smolkas@53693
|
155 |
fun next_label l (next, subst) =
|
blanchet@55907
|
156 |
let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end
|
smolkas@53693
|
157 |
|
blanchet@56641
|
158 |
fun relabel_step (Prove (qs, fix, l, t, subs, (lfs, gfs), meths, comment))
|
blanchet@56641
|
159 |
(accum as (_, subst)) =
|
blanchet@55907
|
160 |
let
|
blanchet@56623
|
161 |
val lfs' = maps (the_list o AList.lookup (op =) subst) lfs
|
blanchet@56623
|
162 |
val ((subs', l'), accum') = accum
|
blanchet@56623
|
163 |
|> fold_map relabel_proof subs
|
blanchet@56623
|
164 |
||>> next_label l
|
blanchet@55907
|
165 |
in
|
blanchet@56641
|
166 |
(Prove (qs, fix, l', t, subs', (lfs', gfs), meths, comment), accum')
|
blanchet@55907
|
167 |
end
|
blanchet@56623
|
168 |
| relabel_step step accum = (step, accum)
|
blanchet@56623
|
169 |
and relabel_proof (Proof (fix, assms, steps)) =
|
blanchet@56623
|
170 |
fold_map (fn (l, t) => next_label l #> apfst (rpair t)) assms
|
blanchet@56623
|
171 |
##>> fold_map relabel_step steps
|
blanchet@56623
|
172 |
#>> (fn (assms, steps) => Proof (fix, assms, steps))
|
smolkas@53693
|
173 |
in
|
blanchet@56621
|
174 |
fst (relabel_proof proof (0, []))
|
smolkas@53693
|
175 |
end
|
smolkas@53693
|
176 |
|
blanchet@56562
|
177 |
val assume_prefix = "a"
|
blanchet@56562
|
178 |
val have_prefix = "f"
|
blanchet@56562
|
179 |
|
blanchet@56624
|
180 |
val relabel_isar_proof_nicely =
|
blanchet@56562
|
181 |
let
|
blanchet@56623
|
182 |
fun next_label depth prefix l (accum as (next, subst)) =
|
blanchet@56562
|
183 |
if l = no_label then
|
blanchet@56623
|
184 |
(l, accum)
|
blanchet@56562
|
185 |
else
|
blanchet@56562
|
186 |
let val l' = (replicate_string (depth + 1) prefix, next) in
|
blanchet@56623
|
187 |
(l', (next + 1, (l, l') :: subst))
|
blanchet@56562
|
188 |
end
|
blanchet@56562
|
189 |
|
blanchet@56641
|
190 |
fun relabel_step depth (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment))
|
blanchet@56641
|
191 |
(accum as (_, subst)) =
|
blanchet@56562
|
192 |
let
|
blanchet@56623
|
193 |
val lfs' = maps (the_list o AList.lookup (op =) subst) lfs
|
blanchet@56651
|
194 |
val (l', accum' as (_, subst')) = next_label depth have_prefix l accum
|
blanchet@56623
|
195 |
val subs' = map (relabel_proof subst' (depth + 1)) subs
|
blanchet@56562
|
196 |
in
|
blanchet@56641
|
197 |
(Prove (qs, xs, l', t, subs', (lfs', gfs), meths, comment), accum')
|
blanchet@56562
|
198 |
end
|
blanchet@56623
|
199 |
| relabel_step _ step accum = (step, accum)
|
blanchet@56562
|
200 |
and relabel_proof subst depth (Proof (fix, assms, steps)) =
|
blanchet@56623
|
201 |
(1, subst)
|
blanchet@56623
|
202 |
|> fold_map (fn (l, t) => next_label depth assume_prefix l #> apfst (rpair t)) assms
|
blanchet@56623
|
203 |
||>> fold_map (relabel_step depth) steps
|
blanchet@56623
|
204 |
|> (fn ((assms, steps), _) => Proof (fix, assms, steps))
|
blanchet@56562
|
205 |
in
|
blanchet@56562
|
206 |
relabel_proof [] 0
|
blanchet@56562
|
207 |
end
|
blanchet@56562
|
208 |
|
blanchet@56553
|
209 |
val indent_size = 2
|
blanchet@56553
|
210 |
|
blanchet@58327
|
211 |
fun string_of_isar_proof ctxt0 i n proof =
|
blanchet@56553
|
212 |
let
|
blanchet@56553
|
213 |
(* Make sure only type constraints inserted by the type annotation code are printed. *)
|
blanchet@58327
|
214 |
val ctxt = ctxt0
|
blanchet@58327
|
215 |
|> Config.put show_markup false
|
blanchet@58327
|
216 |
|> Config.put Printer.show_type_emphasis false
|
blanchet@58327
|
217 |
|> Config.put show_types false
|
blanchet@58327
|
218 |
|> Config.put show_sorts false
|
blanchet@58327
|
219 |
|> Config.put show_consts false
|
blanchet@56553
|
220 |
|
blanchet@56558
|
221 |
fun add_str s' = apfst (suffix s')
|
blanchet@56553
|
222 |
|
blanchet@56553
|
223 |
fun of_indent ind = replicate_string (ind * indent_size) " "
|
blanchet@56553
|
224 |
fun of_moreover ind = of_indent ind ^ "moreover\n"
|
blanchet@56553
|
225 |
fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
|
blanchet@56553
|
226 |
|
blanchet@56553
|
227 |
fun of_obtain qs nr =
|
blanchet@56553
|
228 |
(if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately "
|
blanchet@56553
|
229 |
else if nr = 1 orelse member (op =) qs Then then "then "
|
blanchet@56553
|
230 |
else "") ^ "obtain"
|
blanchet@56553
|
231 |
|
blanchet@56553
|
232 |
fun of_show_have qs = if member (op =) qs Show then "show" else "have"
|
blanchet@56553
|
233 |
fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence"
|
blanchet@56553
|
234 |
|
blanchet@56553
|
235 |
fun of_have qs nr =
|
blanchet@56553
|
236 |
if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " ^ of_show_have qs
|
blanchet@56553
|
237 |
else if nr = 1 orelse member (op =) qs Then then of_thus_hence qs
|
blanchet@56553
|
238 |
else of_show_have qs
|
blanchet@56553
|
239 |
|
blanchet@56553
|
240 |
fun add_term term (s, ctxt) =
|
blanchet@56553
|
241 |
(s ^ (term
|
blanchet@56553
|
242 |
|> singleton (Syntax.uncheck_terms ctxt)
|
blanchet@56555
|
243 |
|> annotate_types_in_term ctxt
|
blanchet@56553
|
244 |
|> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
|
blanchet@56553
|
245 |
|> simplify_spaces
|
blanchet@56553
|
246 |
|> maybe_quote),
|
blanchet@59011
|
247 |
ctxt |> perhaps (try (Variable.auto_fixes term)))
|
blanchet@56553
|
248 |
|
blanchet@58325
|
249 |
fun using_facts [] [] = ""
|
blanchet@58325
|
250 |
| using_facts ls ss = enclose "using " " " (space_implode " " (map string_of_label ls @ ss))
|
blanchet@56599
|
251 |
|
blanchet@56553
|
252 |
(* Local facts are always passed via "using", which affects "meson" and "metis". This is
|
blanchet@56553
|
253 |
arguably stylistically superior, because it emphasises the structure of the proof. It is also
|
blanchet@56553
|
254 |
more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence"
|
blanchet@56553
|
255 |
and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *)
|
blanchet@58629
|
256 |
fun of_method ls ss meth =
|
blanchet@58629
|
257 |
let val direct = is_proof_method_direct meth in
|
blanchet@56623
|
258 |
using_facts ls (if direct then [] else ss) ^
|
blanchet@58629
|
259 |
"by " ^ string_of_proof_method ctxt (if direct then ss else []) meth
|
blanchet@56623
|
260 |
end
|
blanchet@56553
|
261 |
|
blanchet@56553
|
262 |
fun of_free (s, T) =
|
blanchet@56553
|
263 |
maybe_quote s ^ " :: " ^
|
blanchet@56553
|
264 |
maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T))
|
blanchet@56553
|
265 |
|
blanchet@56553
|
266 |
fun add_frees xs (s, ctxt) =
|
blanchet@59011
|
267 |
(s ^ space_implode " and " (map of_free xs), ctxt |> fold Variable.auto_fixes (map Free xs))
|
blanchet@56553
|
268 |
|
blanchet@56553
|
269 |
fun add_fix _ [] = I
|
blanchet@56623
|
270 |
| add_fix ind xs = add_str (of_indent ind ^ "fix ") #> add_frees xs #> add_str "\n"
|
blanchet@56553
|
271 |
|
blanchet@56553
|
272 |
fun add_assm ind (l, t) =
|
blanchet@56623
|
273 |
add_str (of_indent ind ^ "assume " ^ of_label l) #> add_term t #> add_str "\n"
|
blanchet@56553
|
274 |
|
blanchet@56553
|
275 |
fun of_subproof ind ctxt proof =
|
blanchet@56553
|
276 |
let
|
blanchet@56553
|
277 |
val ind = ind + 1
|
blanchet@56553
|
278 |
val s = of_proof ind ctxt proof
|
blanchet@56553
|
279 |
val prefix = "{ "
|
blanchet@56553
|
280 |
val suffix = " }"
|
blanchet@56553
|
281 |
in
|
blanchet@56553
|
282 |
replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
|
blanchet@56553
|
283 |
String.extract (s, ind * indent_size, SOME (size s - ind * indent_size - 1)) ^
|
blanchet@56553
|
284 |
suffix ^ "\n"
|
blanchet@56553
|
285 |
end
|
blanchet@56553
|
286 |
and of_subproofs _ _ _ [] = ""
|
blanchet@56623
|
287 |
| of_subproofs ind ctxt qs subs =
|
blanchet@56553
|
288 |
(if member (op =) qs Then then of_moreover ind else "") ^
|
blanchet@56623
|
289 |
space_implode (of_moreover ind) (map (of_subproof ind ctxt) subs)
|
blanchet@56623
|
290 |
and add_step_pre ind qs subs (s, ctxt) =
|
blanchet@56623
|
291 |
(s ^ of_subproofs ind ctxt qs subs ^ of_indent ind, ctxt)
|
blanchet@56553
|
292 |
and add_step ind (Let (t1, t2)) =
|
blanchet@56558
|
293 |
add_str (of_indent ind ^ "let ")
|
blanchet@56623
|
294 |
#> add_term t1 #> add_str " = " #> add_term t2 #> add_str "\n"
|
blanchet@56651
|
295 |
| add_step ind (Prove (qs, xs, l, t, subs, (ls, ss), meth :: _, comment)) =
|
blanchet@56623
|
296 |
add_step_pre ind qs subs
|
blanchet@56553
|
297 |
#> (case xs of
|
blanchet@56623
|
298 |
[] => add_str (of_have qs (length subs) ^ " ")
|
blanchet@56623
|
299 |
| _ => add_str (of_obtain qs (length subs) ^ " ") #> add_frees xs #> add_str " where ")
|
blanchet@56559
|
300 |
#> add_str (of_label l)
|
blanchet@56559
|
301 |
#> add_term t
|
blanchet@56559
|
302 |
#> add_str (" " ^
|
blanchet@58629
|
303 |
of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^
|
blanchet@56641
|
304 |
(if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n")
|
blanchet@56553
|
305 |
and add_steps ind = fold (add_step ind)
|
blanchet@56553
|
306 |
and of_proof ind ctxt (Proof (xs, assms, steps)) =
|
blanchet@56623
|
307 |
("", ctxt)
|
blanchet@56623
|
308 |
|> add_fix ind xs
|
blanchet@56623
|
309 |
|> fold (add_assm ind) assms
|
blanchet@56623
|
310 |
|> add_steps ind steps
|
blanchet@56623
|
311 |
|> fst
|
blanchet@56553
|
312 |
in
|
blanchet@58628
|
313 |
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
|
blanchet@58629
|
314 |
of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
|
blanchet@58629
|
315 |
of_indent 0 ^ (if n = 1 then "qed" else "next")
|
blanchet@56553
|
316 |
end
|
blanchet@56553
|
317 |
|
blanchet@55877
|
318 |
end;
|