equal
deleted
inserted
replaced
263 in () end |
263 in () end |
264 |
264 |
265 |
265 |
266 (* Isar command *) |
266 (* Isar command *) |
267 |
267 |
|
268 (*WAS in Isabelle2020 |
|
269 val _ = |
|
270 Outer_Syntax.command \<^command_keyword>\<open>boogie_file\<close> |
|
271 "prove verification condition from .b2i file" |
|
272 (Resources.provide_parse_files "boogie_file" >> (fn files => |
|
273 Toplevel.theory (fn thy => |
|
274 let |
|
275 val ([{lines, ...}], thy') = files thy; |
|
276 val _ = boogie_prove thy' lines; |
|
277 in thy' end))) |
|
278 *) |
268 val _ = |
279 val _ = |
269 Outer_Syntax.command \<^command_keyword>\<open>boogie_file\<close> |
280 Outer_Syntax.command \<^command_keyword>\<open>boogie_file\<close> |
270 "prove verification condition from .b2i file" |
281 "prove verification condition from .b2i file" |
271 (Resources.provide_parse_file >> (fn get_file => |
282 (Resources.provide_parse_file >> (fn get_file => |
272 Toplevel.theory (fn thy => |
283 Toplevel.theory (fn thy => |