equal
deleted
inserted
replaced
148 |
148 |
149 fun invoke_try thy t = |
149 fun invoke_try thy t = |
150 let |
150 let |
151 val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy) |
151 val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy) |
152 in |
152 in |
153 case Try.invoke_try (SOME (seconds 5.0)) state of |
153 case Try.invoke_try (SOME (seconds 5.0)) ([], [], []) state of |
154 true => (Solved, ([], NONE)) |
154 true => (Solved, ([], NONE)) |
155 | false => (Unsolved, ([], NONE)) |
155 | false => (Unsolved, ([], NONE)) |
156 end |
156 end |
157 |
157 |
158 val try_mtd = ("try", invoke_try) |
158 val try_mtd = ("try", invoke_try) |