40 val goal_tac: thm -> int -> tactic |
40 val goal_tac: thm -> int -> tactic |
41 val refine_goals: (context -> thm -> unit) -> context -> thm list -> state -> state Seq.seq |
41 val refine_goals: (context -> thm -> unit) -> context -> thm list -> state -> state Seq.seq |
42 val raw_goal: state -> {context: context, facts: thm list, goal: thm} |
42 val raw_goal: state -> {context: context, facts: thm list, goal: thm} |
43 val goal: state -> {context: context, facts: thm list, goal: thm} |
43 val goal: state -> {context: context, facts: thm list, goal: thm} |
44 val simple_goal: state -> {context: context, goal: thm} |
44 val simple_goal: state -> {context: context, goal: thm} |
|
45 val status_markup: state -> Markup.T |
45 val let_bind: (term list * term) list -> state -> state |
46 val let_bind: (term list * term) list -> state -> state |
46 val let_bind_cmd: (string list * string) list -> state -> state |
47 val let_bind_cmd: (string list * string) list -> state -> state |
47 val write: Syntax.mode -> (term * mixfix) list -> state -> state |
48 val write: Syntax.mode -> (term * mixfix) list -> state -> state |
48 val write_cmd: Syntax.mode -> (string * mixfix) list -> state -> state |
49 val write_cmd: Syntax.mode -> (string * mixfix) list -> state -> state |
49 val fix: (binding * typ option * mixfix) list -> state -> state |
50 val fix: (binding * typ option * mixfix) list -> state -> state |
518 let |
519 let |
519 val (_, (facts, _)) = get_goal state; |
520 val (_, (facts, _)) = get_goal state; |
520 val (ctxt, (_, goal)) = get_goal (refine_insert facts state); |
521 val (ctxt, (_, goal)) = get_goal (refine_insert facts state); |
521 in {context = ctxt, goal = goal} end; |
522 in {context = ctxt, goal = goal} end; |
522 |
523 |
|
524 fun status_markup state = |
|
525 (case try goal state of |
|
526 SOME {goal, ...} => Markup.proof_state (Thm.nprems_of goal) |
|
527 | NONE => Markup.empty); |
|
528 |
523 |
529 |
524 |
530 |
525 (*** structured proof commands ***) |
531 (*** structured proof commands ***) |
526 |
532 |
527 (** context elements **) |
533 (** context elements **) |