equal
deleted
inserted
replaced
29 val assert_forward_or_chain: state -> state |
29 val assert_forward_or_chain: state -> state |
30 val assert_backward: state -> state |
30 val assert_backward: state -> state |
31 val assert_no_chain: state -> state |
31 val assert_no_chain: state -> state |
32 val enter_forward: state -> state |
32 val enter_forward: state -> state |
33 val get_goal: state -> context * (thm list * thm) |
33 val get_goal: state -> context * (thm list * thm) |
|
34 val schematic_goal: state -> bool |
34 val show_main_goal: bool ref |
35 val show_main_goal: bool ref |
35 val verbose: bool ref |
36 val verbose: bool ref |
36 val pretty_state: int -> state -> Pretty.T list |
37 val pretty_state: int -> state -> Pretty.T list |
37 val pretty_goals: bool -> state -> Pretty.T list |
38 val pretty_goals: bool -> state -> Pretty.T list |
38 val refine: Method.text -> state -> state Seq.seq |
39 val refine: Method.text -> state -> state Seq.seq |
304 |
305 |
305 fun get_goal state = |
306 fun get_goal state = |
306 let val (ctxt, (_, {using, goal, ...})) = find_goal state |
307 let val (ctxt, (_, {using, goal, ...})) = find_goal state |
307 in (ctxt, (using, goal)) end; |
308 in (ctxt, (using, goal)) end; |
308 |
309 |
|
310 fun schematic_goal state = |
|
311 let |
|
312 val (_, (_, {statement = (_, propss), ...})) = find_goal state; |
|
313 val tvars = fold (fold Term.add_tvars) propss []; |
|
314 val vars = fold (fold Term.add_vars) propss []; |
|
315 in not (null tvars andalso null vars) end; |
|
316 |
309 |
317 |
310 |
318 |
311 (** pretty_state **) |
319 (** pretty_state **) |
312 |
320 |
313 val show_main_goal = ref false; |
321 val show_main_goal = ref false; |