author  paulson 
Tue, 22 Jul 1997 11:14:18 +0200  
changeset 3538  ed9de44032e0 
parent 3536  8fb4150e2ad3 
child 3669  3384c6f1f095 
permissions  rwrr 
1460  1 
(* Title: Pure/goals.ML 
0  2 
ID: $Id$ 
1460  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1993 University of Cambridge 
5 

6 
Goal stack package. The goal stack initially holds a dummy proof, and can 

7 
never become empty. Each goal stack consists of a list of levels. The 

8 
undo list is a list of goal stacks. Finally, there may be a stack of 

9 
pending proofs. 

10 
*) 

11 

12 

13 
signature GOALS = 

14 
sig 

15 
type proof 

1460  16 
val ba : int > unit 
17 
val back : unit > unit 

18 
val bd : thm > int > unit 

19 
val bds : thm list > int > unit 

20 
val be : thm > int > unit 

21 
val bes : thm list > int > unit 

22 
val br : thm > int > unit 

23 
val brs : thm list > int > unit 

24 
val bw : thm > unit 

25 
val bws : thm list > unit 

26 
val by : tactic > unit 

27 
val byev : tactic list > unit 

28 
val chop : unit > unit 

29 
val choplev : int > unit 

30 
val fa : unit > unit 

31 
val fd : thm > unit 

32 
val fds : thm list > unit 

33 
val fe : thm > unit 

34 
val fes : thm list > unit 

35 
val filter_goal : (term*term>bool) > thm list > int > thm list 

36 
val fr : thm > unit 

37 
val frs : thm list > unit 

38 
val getgoal : int > term 

39 
val gethyps : int > thm list 

40 
val goal : theory > string > thm list 

41 
val goalw : theory > thm list > string > thm list 

42 
val goalw_cterm : thm list > cterm > thm list 

3532  43 
val print_current_goals_fn : (int > int > thm > unit) ref 
1460  44 
val pop_proof : unit > thm list 
45 
val pr : unit > unit 

2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2514
diff
changeset

46 
val prlev : int > unit 
2514  47 
val prlim : int > unit 
1628
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

48 
val pr_latex : unit > unit 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

49 
val printgoal_latex : int > unit 
1460  50 
val premises : unit > thm list 
51 
val prin : term > unit 

52 
val printyp : typ > unit 

53 
val pprint_term : term > pprint_args > unit 

54 
val pprint_typ : typ > pprint_args > unit 

55 
val print_exn : exn > 'a 

56 
val print_sign_exn : Sign.sg > exn > 'a 

57 
val proof_timing : bool ref 

58 
val prove_goal : theory > string > (thm list > tactic list) > thm 

577  59 
val prove_goalw : theory>thm list>string>(thm list>tactic list)>thm 
1460  60 
val prove_goalw_cterm : thm list>cterm>(thm list>tactic list)>thm 
61 
val push_proof : unit > unit 

62 
val read : string > term 

63 
val ren : string > int > unit 

64 
val restore_proof : proof > thm list 

65 
val result : unit > thm 

3532  66 
val result_error_fn : (thm > string > thm) ref 
1460  67 
val rotate_proof : unit > thm list 
68 
val uresult : unit > thm 

69 
val save_proof : unit > proof 

70 
val topthm : unit > thm 

71 
val undo : unit > unit 

0  72 
end; 
73 

1500  74 
structure Goals : GOALS = 
0  75 
struct 
76 

77 
(*Each level of goal stack includes a proof state and alternative states, 

78 
the output of the tactic applied to the preceeding level. *) 

79 
type gstack = (thm * thm Sequence.seq) list; 

80 

81 
datatype proof = Proof of gstack list * thm list * (bool*thm>thm); 

82 

83 
(*** References ***) 

84 

85 
(*Should process time be printed after proof steps?*) 

86 
val proof_timing = ref false; 

87 

88 
(*Current assumption list  set by "goal".*) 

89 
val curr_prems = ref([] : thm list); 

90 

91 
(*Return assumption list  useful if you didn't save "goal"'s result. *) 

92 
fun premises() = !curr_prems; 

93 

94 
(*Current result maker  set by "goal", used by "result". *) 

95 
val curr_mkresult = 

96 
ref((fn _=> error"No goal has been supplied in subgoal module") 

97 
: bool*thm>thm); 

98 

2878
bf7b6833e4d7
changed signature of dummy goal from proto_pure to pure;
wenzelm
parents:
2580
diff
changeset

99 
val dummy = trivial(read_cterm Sign.pure 
0  100 
("PROP No_goal_has_been_supplied",propT)); 
101 

102 
(*List of previous goal stacks, for the undo operation. Set by setstate. 

103 
A list of lists!*) 

104 
val undo_list = ref([[(dummy, Sequence.null)]] : gstack list); 

105 

106 
(* Stack of proof attempts *) 

107 
val proofstack = ref([]: proof list); 

108 

109 

110 
(*** Setting up goaldirected proof ***) 

111 

112 
(*Generates the list of new theories when the proof state's signature changes*) 

113 
fun sign_error (sign,sign') = 

114 
let val stamps = #stamps(Sign.rep_sg sign') \\ 

115 
#stamps(Sign.rep_sg sign) 

116 
in case stamps of 

117 
[stamp] => "\nNew theory: " ^ !stamp 

118 
 _ => "\nNew theories: " ^ space_implode ", " (map ! stamps) 

119 
end; 

120 

1928  121 
(*Default action is to print an error message; could be suppressed for 
122 
special applications.*) 

123 
fun result_error_default state msg : thm = 

124 
(writeln ("Bad final proof state:"); 

125 
!print_goals_ref (!goals_limit) state; 

3532  126 
writeln msg; raise ERROR); 
1928  127 

3532  128 
val result_error_fn = ref result_error_default; 
1928  129 

0  130 
(*Common treatment of "goal" and "prove_goal": 
131 
Return assumptions, initial proof state, and function to make result. *) 

132 
fun prepare_proof rths chorn = 

230  133 
let val {sign, t=horn,...} = rep_cterm chorn; 
0  134 
val (_,As,B) = Logic.strip_horn(horn); 
230  135 
val cAs = map (cterm_of sign) As; 
1413  136 
val prems = map (rewrite_rule rths o forall_elim_vars(0) o assume) cAs 
137 
and st0 = (rewrite_goals_rule rths o trivial) (cterm_of sign B) 

0  138 
(*discharges assumptions from state in the order they appear in goal; 
1460  139 
checks (if requested) that resulting theorem is equivalent to goal. *) 
0  140 
fun mkresult (check,state) = 
696
eb5b42442b14
Pure/goals/prepare_proof/mkresult: now smashes flexflex pairs in the final
lcp
parents:
678
diff
changeset

141 
let val state = Sequence.hd (flexflex_rule state) 
1565  142 
handle THM _ => state (*smash flexflex pairs*) 
1460  143 
val ngoals = nprems_of state 
1219  144 
val th = strip_shyps (implies_intr_list cAs state) 
1240  145 
val {hyps,prop,sign=sign',...} = rep_thm th 
146 
val xshyps = extra_shyps th; 

2169
31ba286f2307
Removed "standard" call from uresult, to allow specialist applications
paulson
parents:
2126
diff
changeset

147 
in if not check then th 
3532  148 
else if not (Sign.eq_sg(sign,sign')) then !result_error_fn state 
1460  149 
("Signature of proof state has changed!" ^ 
150 
sign_error (sign,sign')) 

3532  151 
else if ngoals>0 then !result_error_fn state 
1460  152 
(string_of_int ngoals ^ " unsolved goals!") 
3532  153 
else if not (null hyps) then !result_error_fn state 
0  154 
("Additional hypotheses:\n" ^ 
155 
cat_lines (map (Sign.string_of_term sign) hyps)) 

3532  156 
else if not (null xshyps) then !result_error_fn state 
1240  157 
("Extra sort hypotheses: " ^ 
2962  158 
commas (map Sorts.str_of_sort xshyps)) 
1460  159 
else if Pattern.matches (#tsig(Sign.rep_sg sign)) 
160 
(term_of chorn, prop) 

161 
then standard th 

3532  162 
else !result_error_fn state "proved a different theorem" 
0  163 
end 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
577
diff
changeset

164 
in 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
577
diff
changeset

165 
if Sign.eq_sg(sign, #sign(rep_thm st0)) 
0  166 
then (prems, st0, mkresult) 
167 
else error ("Definitions would change the proof state's signature" ^ 

1460  168 
sign_error (sign, #sign(rep_thm st0))) 
0  169 
end 
170 
handle THM(s,_,_) => error("prepare_proof: exception THM was raised!\n" ^ s); 

171 

172 
(*Prints exceptions readably to users*) 

577  173 
fun print_sign_exn_unit sign e = 
0  174 
case e of 
175 
THM (msg,i,thms) => 

1460  176 
(writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg); 
177 
seq print_thm thms) 

0  178 
 THEORY (msg,thys) => 
1460  179 
(writeln ("Exception THEORY raised:\n" ^ msg); 
180 
seq print_theory thys) 

0  181 
 TERM (msg,ts) => 
1460  182 
(writeln ("Exception TERM raised:\n" ^ msg); 
183 
seq (writeln o Sign.string_of_term sign) ts) 

0  184 
 TYPE (msg,Ts,ts) => 
1460  185 
(writeln ("Exception TYPE raised:\n" ^ msg); 
186 
seq (writeln o Sign.string_of_typ sign) Ts; 

187 
seq (writeln o Sign.string_of_term sign) ts) 

0  188 
 e => raise e; 
189 

577  190 
(*Prints an exception, then fails*) 
191 
fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise ERROR); 

192 

0  193 
(** the prove_goal.... commands 
194 
Prove theorem using the listed tactics; check it has the specified form. 

195 
Augment signature with all type assignments of goal. 

196 
Syntax is similar to "goal" command for easy keyboard use. **) 

197 

198 
(*Version taking the goal as a cterm*) 

199 
fun prove_goalw_cterm rths chorn tacsf = 

200 
let val (prems, st0, mkresult) = prepare_proof rths chorn 

201 
val tac = EVERY (tacsf prems) 

202 
fun statef() = 

1500  203 
(case Sequence.pull (tac st0) of 
1460  204 
Some(st,_) => st 
205 
 _ => error ("prove_goal: tactic failed")) 

545
fc4ff96bb0e9
Pure/goals.ML: prove_goalw_cterm now does its own exceptionhandling, moved
lcp
parents:
253
diff
changeset

206 
in mkresult (true, cond_timeit (!proof_timing) statef) end 
914
cae574c09137
Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest
lcp
parents:
696
diff
changeset

207 
handle e => (print_sign_exn_unit (#sign (rep_cterm chorn)) e; 
1460  208 
error ("The exception above was raised for\n" ^ 
209 
string_of_cterm chorn)); 

545
fc4ff96bb0e9
Pure/goals.ML: prove_goalw_cterm now does its own exceptionhandling, moved
lcp
parents:
253
diff
changeset

210 

0  211 

212 
(*Version taking the goal as a string*) 

213 
fun prove_goalw thy rths agoal tacsf = 

214 
let val sign = sign_of thy 

230  215 
val chorn = read_cterm sign (agoal,propT) 
545
fc4ff96bb0e9
Pure/goals.ML: prove_goalw_cterm now does its own exceptionhandling, moved
lcp
parents:
253
diff
changeset

216 
in prove_goalw_cterm rths chorn tacsf end 
fc4ff96bb0e9
Pure/goals.ML: prove_goalw_cterm now does its own exceptionhandling, moved
lcp
parents:
253
diff
changeset

217 
handle ERROR => error (*from read_cterm?*) 
3536  218 
("The error(s) above occurred for " ^ quote agoal); 
0  219 

220 
(*String version with no metarewriterules*) 

221 
fun prove_goal thy = prove_goalw thy []; 

222 

223 

224 
(*** Commands etc ***) 

225 

226 
(*Return the current goal stack, if any, from undo_list*) 

227 
fun getstate() : gstack = case !undo_list of 

228 
[] => error"No current state in subgoal module" 

229 
 x::_ => x; 

230 

231 
(*Pops the given goal stack*) 

232 
fun pop [] = error"Cannot go back past the beginning of the proof!" 

233 
 pop (pair::pairs) = (pair,pairs); 

234 

235 

3532  236 
(*Print goals of current level*) 
237 
fun print_current_goals_default n max th = 

238 
(writeln ("Level " ^ string_of_int n); !print_goals_ref max th); 

239 

240 
val print_current_goals_fn = ref print_current_goals_default; 

241 

0  242 
(*Print a level of the goal stack.*) 
3532  243 
fun print_top ((th, _), pairs) = 
244 
!print_current_goals_fn (length pairs) (!goals_limit) th; 

0  245 

246 
(*Printing can raise exceptions, so the assignment occurs last. 

247 
Can do setstate[(st,Sequence.null)] to set st as the state. *) 

248 
fun setstate newgoals = 

249 
(print_top (pop newgoals); undo_list := newgoals :: !undo_list); 

250 

251 
(*Given a proof state transformation, return a command that updates 

252 
the goal stack*) 

253 
fun make_command com = setstate (com (pop (getstate()))); 

254 

255 
(*Apply a function on proof states to the current goal stack*) 

256 
fun apply_fun f = f (pop(getstate())); 

257 

258 
(*Return the top theorem, representing the proof state*) 

259 
fun topthm () = apply_fun (fn ((th,_), _) => th); 

260 

261 
(*Return the final result. *) 

262 
fun result () = !curr_mkresult (true, topthm()); 

263 

264 
(*Return the result UNCHECKED that it equals the goal  for synthesis, 

265 
answer extraction, or other instantiation of Vars *) 

266 
fun uresult () = !curr_mkresult (false, topthm()); 

267 

268 
(*Get subgoal i from goal stack*) 

2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2514
diff
changeset

269 
fun getgoal i = List.nth (prems_of (topthm()), i1) 
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2514
diff
changeset

270 
handle Subscript => error"getgoal: Goal number out of range"; 
0  271 

272 
(*Return subgoal i's hypotheses as metalevel assumptions. 

273 
For debugging uses of METAHYPS*) 

274 
local exception GETHYPS of thm list 

275 
in 

276 
fun gethyps i = 

1500  277 
(METAHYPS (fn hyps => raise (GETHYPS hyps)) i (topthm()); []) 
0  278 
handle GETHYPS hyps => hyps 
279 
end; 

280 

281 
(*Which thms could apply to goal i? (debugs tactics involving filter_thms) *) 

282 
fun filter_goal could ths i = filter_thms could (999, getgoal i, ths); 

283 

284 
(*For inspecting earlier levels of the backward proof*) 

285 
fun chop_level n (pair,pairs) = 

286 
let val level = length pairs 

2126
d927beecedf8
Allowing negative levels (as offsets) in prlev and choplev
paulson
parents:
1928
diff
changeset

287 
in if n<0 andalso ~n <= level 
2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2514
diff
changeset

288 
then List.drop (pair::pairs, ~n) 
2126
d927beecedf8
Allowing negative levels (as offsets) in prlev and choplev
paulson
parents:
1928
diff
changeset

289 
else if 0<=n andalso n<= level 
2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2514
diff
changeset

290 
then List.drop (pair::pairs, level  n) 
0  291 
else error ("Level number must lie between 0 and " ^ 
1460  292 
string_of_int level) 
0  293 
end; 
294 

2514  295 
(*Print the given level of the proof; prlev ~1 prints previous level*) 
0  296 
fun prlev n = apply_fun (print_top o pop o (chop_level n)); 
297 
fun pr () = apply_fun print_top; 

298 

2514  299 
(*Set goals_limit and print again*) 
300 
fun prlim n = (goals_limit:=n; pr()); 

301 

0  302 
(** the goal.... commands 
303 
Read main goal. Set global variables curr_prems, curr_mkresult. 

304 
Initial subgoal and premises are rewritten using rths. **) 

305 

306 
(*Version taking the goal as a cterm; if you have a term t and theory thy, use 

230  307 
goalw_cterm rths (cterm_of (sign_of thy) t); *) 
0  308 
fun goalw_cterm rths chorn = 
309 
let val (prems, st0, mkresult) = prepare_proof rths chorn 

310 
in undo_list := []; 

311 
setstate [ (st0, Sequence.null) ]; 

312 
curr_prems := prems; 

313 
curr_mkresult := mkresult; 

314 
prems 

315 
end; 

316 

317 
(*Version taking the goal as a string*) 

318 
fun goalw thy rths agoal = 

230  319 
goalw_cterm rths (read_cterm(sign_of thy)(agoal,propT)) 
0  320 
handle ERROR => error (*from type_assign, etc via prepare_proof*) 
3536  321 
("The error(s) above occurred for " ^ quote agoal); 
0  322 

323 
(*String version with no metarewriterules*) 

324 
fun goal thy = goalw thy []; 

325 

326 
(*Proof step "by" the given tactic  apply tactic to the proof state*) 

327 
fun by_com tac ((th,ths), pairs) : gstack = 

1500  328 
(case Sequence.pull(tac th) of 
0  329 
None => error"by: tactic failed" 
330 
 Some(th2,ths2) => 

331 
(if eq_thm(th,th2) 

3532  332 
then writeln "Warning: same as previous level" 
1460  333 
else if eq_thm_sg(th,th2) then () 
3532  334 
else writeln ("Warning: signature of proof state has changed" ^ 
1460  335 
sign_error (#sign(rep_thm th), #sign(rep_thm th2))); 
0  336 
((th2,ths2)::(th,ths)::pairs))); 
337 

338 
fun by tac = cond_timeit (!proof_timing) 

339 
(fn() => make_command (by_com tac)); 

340 

341 
(* byev[tac1,...,tacn] applies tac1 THEN ... THEN tacn. 

342 
Good for debugging proofs involving prove_goal.*) 

343 
val byev = by o EVERY; 

344 

345 

346 
(*Backtracking means find an alternative result from a tactic. 

347 
If none at this level, try earlier levels*) 

348 
fun backtrack [] = error"back: no alternatives" 

349 
 backtrack ((th,thstr) :: pairs) = 

350 
(case Sequence.pull thstr of 

1460  351 
None => (writeln"Going back a level..."; backtrack pairs) 
352 
 Some(th2,thstr2) => 

353 
(if eq_thm(th,th2) 

3532  354 
then writeln "Warning: same as previous choice at this level" 
1460  355 
else if eq_thm_sg(th,th2) then () 
3532  356 
else writeln "Warning: signature of proof state has changed"; 
1460  357 
(th2,thstr2)::pairs)); 
0  358 

359 
fun back() = setstate (backtrack (getstate())); 

360 

361 
(*Chop back to previous level of the proof*) 

362 
fun choplev n = make_command (chop_level n); 

363 

364 
(*Chopping back the goal stack*) 

365 
fun chop () = make_command (fn (_,pairs) => pairs); 

366 

367 
(*Restore the previous proof state; discard current state. *) 

368 
fun undo() = case !undo_list of 

369 
[] => error"No proof state" 

370 
 [_] => error"Already at initial state" 

371 
 _::newundo => (undo_list := newundo; pr()) ; 

372 

373 

374 
(*** Managing the proof stack ***) 

375 

376 
fun save_proof() = Proof(!undo_list, !curr_prems, !curr_mkresult); 

377 

378 
fun restore_proof(Proof(ul,prems,mk)) = 

379 
(undo_list:= ul; curr_prems:= prems; curr_mkresult := mk; prems); 

380 

381 

382 
fun top_proof() = case !proofstack of 

1460  383 
[] => error("Stack of proof attempts is empty!") 
0  384 
 p::ps => (p,ps); 
385 

386 
(* push a copy of the current proof state on to the stack *) 

387 
fun push_proof() = (proofstack := (save_proof() :: !proofstack)); 

388 

389 
(* discard the top proof state of the stack *) 

390 
fun pop_proof() = 

391 
let val (p,ps) = top_proof() 

392 
val prems = restore_proof p 

393 
in proofstack := ps; pr(); prems end; 

394 

395 
(* rotate the stack so that the top element goes to the bottom *) 

396 
fun rotate_proof() = let val (p,ps) = top_proof() 

1460  397 
in proofstack := ps@[save_proof()]; 
398 
restore_proof p; 

399 
pr(); 

400 
!curr_prems 

401 
end; 

0  402 

403 

404 
(** Shortcuts for commonlyused tactics **) 

405 

406 
fun bws rls = by (rewrite_goals_tac rls); 

407 
fun bw rl = bws [rl]; 

408 

409 
fun brs rls i = by (resolve_tac rls i); 

410 
fun br rl = brs [rl]; 

411 

412 
fun bes rls i = by (eresolve_tac rls i); 

413 
fun be rl = bes [rl]; 

414 

415 
fun bds rls i = by (dresolve_tac rls i); 

416 
fun bd rl = bds [rl]; 

417 

418 
fun ba i = by (assume_tac i); 

419 

420 
fun ren str i = by (rename_tac str i); 

421 

422 
(** Shortcuts to work on the first applicable subgoal **) 

423 

424 
fun frs rls = by (FIRSTGOAL (trace_goalno_tac (resolve_tac rls))); 

425 
fun fr rl = frs [rl]; 

426 

427 
fun fes rls = by (FIRSTGOAL (trace_goalno_tac (eresolve_tac rls))); 

428 
fun fe rl = fes [rl]; 

429 

430 
fun fds rls = by (FIRSTGOAL (trace_goalno_tac (dresolve_tac rls))); 

431 
fun fd rl = fds [rl]; 

432 

433 
fun fa() = by (FIRSTGOAL (trace_goalno_tac assume_tac)); 

434 

435 
(** Reading and printing terms wrt the current theory **) 

436 

437 
fun top_sg() = #sign(rep_thm(topthm())); 

438 

230  439 
fun read s = term_of (read_cterm (top_sg()) 
1460  440 
(s, (TVar(("DUMMY",0),[])))); 
0  441 

442 
(*Print a term under the current signature of the proof state*) 

443 
fun prin t = writeln (Sign.string_of_term (top_sg()) t); 

444 

445 
fun printyp T = writeln (Sign.string_of_typ (top_sg()) T); 

446 

447 
fun pprint_term t = Sign.pprint_term (top_sg()) t; 

448 

449 
fun pprint_typ T = Sign.pprint_typ (top_sg()) T; 

450 

1628
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

451 
(* Redirect output of function f:unit>unit to LaTeX *) 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

452 
fun redirect_to_latex f = 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

453 
let 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

454 
val s = ref "" 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

455 
val old_prs_fn = !prs_fn 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

456 
in 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

457 
(prs_fn := (fn a => s := !s ^ a); 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

458 
f (); 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

459 
latex (!s); 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

460 
prs_fn := old_prs_fn) 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

461 
end; 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

462 

60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

463 
(* Display current proof state in xdvi window *) 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

464 
fun pr_latex () = redirect_to_latex pr; 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

465 

60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

466 
(* Display goal n of current proof state in xdvi window *) 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

467 
fun printgoal_latex n = redirect_to_latex (fn () => prin(getgoal n)); 
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset

468 

0  469 
(*Prints exceptions nicely at top level; 
470 
raises the exception in order to have a polymorphic type!*) 

914
cae574c09137
Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest
lcp
parents:
696
diff
changeset

471 
fun print_exn e = (print_sign_exn_unit (top_sg()) e; raise e); 
0  472 

473 
end; 

1500  474 

475 
open Goals; 