equal
deleted
inserted
replaced
5 (*<*) |
5 (*<*) |
6 theory Overview |
6 theory Overview |
7 imports Imperative_HOL "HOL-Library.LaTeXsugar" |
7 imports Imperative_HOL "HOL-Library.LaTeXsugar" |
8 begin |
8 begin |
9 |
9 |
10 (* type constraints with spacing *) |
10 unbundle constrain_space_syntax |
11 no_syntax (output) |
|
12 "_constrain" :: "logic => type => logic" (\<open>_::_\<close> [4, 0] 3) |
|
13 "_constrain" :: "prop' => type => prop'" (\<open>_::_\<close> [4, 0] 3) |
|
14 |
|
15 syntax (output) |
|
16 "_constrain" :: "logic => type => logic" (\<open>_ :: _\<close> [4, 0] 3) |
|
17 "_constrain" :: "prop' => type => prop'" (\<open>_ :: _\<close> [4, 0] 3) |
|
18 (*>*) |
11 (*>*) |
19 |
12 |
20 text \<open> |
13 text \<open> |
21 \<open>Imperative HOL\<close> is a lightweight framework for reasoning |
14 \<open>Imperative HOL\<close> is a lightweight framework for reasoning |
22 about imperative data structures in \<open>Isabelle/HOL\<close> |
15 about imperative data structures in \<open>Isabelle/HOL\<close> |