equal
deleted
inserted
replaced
154 fun subgoals 0 = "" |
154 fun subgoals 0 = "" |
155 | subgoals 1 = "goal (1 subgoal):" |
155 | subgoals 1 = "goal (1 subgoal):" |
156 | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):" |
156 | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):" |
157 |
157 |
158 val state = proof_state node |
158 val state = proof_state node |
159 val goals = Goal_Display.pretty_goal {main = false, limit = false} ctxt state |
159 val goals = Goal_Display.pretty_goal ctxt state |
160 |
160 |
161 val {prop, ...} = rep_thm state; |
161 val {prop, ...} = rep_thm state; |
162 val (As, _) = Logic.strip_horn prop; |
162 val (As, _) = Logic.strip_horn prop; |
163 val output = (case (length As) of |
163 val output = (case (length As) of |
164 0 => [goals] |
164 0 => [goals] |