equal
deleted
inserted
replaced
124 datatype proof_attempt = Solved of thm | Stuck of thm | Fail |
124 datatype proof_attempt = Solved of thm | Stuck of thm | Fail |
125 |
125 |
126 fun try_proof cgoal tac = |
126 fun try_proof cgoal tac = |
127 case SINGLE tac (Goal.init cgoal) of |
127 case SINGLE tac (Goal.init cgoal) of |
128 NONE => Fail |
128 NONE => Fail |
129 | SOME st => if Thm.no_prems st then Solved (Goal.finish st) else Stuck st |
129 | SOME st => |
|
130 if Thm.no_prems st |
|
131 then Solved (Goal.finish (Syntax.init_pretty_global (Thm.theory_of_cterm cgoal)) st) |
|
132 else Stuck st |
130 |
133 |
131 |
134 |
132 fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) = |
135 fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) = |
133 if cn = n then dest_binop_list cn a @ dest_binop_list cn b else [ t ] |
136 if cn = n then dest_binop_list cn a @ dest_binop_list cn b else [ t ] |
134 | dest_binop_list _ t = [ t ] |
137 | dest_binop_list _ t = [ t ] |