| changeset 35105 | 1822c658a5e4 |
| parent 34181 | 003333ffa543 |
| child 36899 | bcd6fce5bf06 |
| 35102:cc7a0b9f938c | 35105:1822c658a5e4 |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Integration of the Boogie program verifier *} |
5 header {* Integration of the Boogie program verifier *} |
6 |
6 |
7 theory Boogie |
7 theory Boogie |
8 imports SMT |
8 imports "~~/src/HOL/SMT/SMT" |
9 uses |
9 uses |
10 ("Tools/boogie_vcs.ML") |
10 ("Tools/boogie_vcs.ML") |
11 ("Tools/boogie_loader.ML") |
11 ("Tools/boogie_loader.ML") |
12 ("Tools/boogie_tactics.ML") |
12 ("Tools/boogie_tactics.ML") |
13 ("Tools/boogie_commands.ML") |
13 ("Tools/boogie_commands.ML") |