| changeset 61143 | 5f898411ce87 |
| parent 59938 | f84b93187ab6 |
| child 62969 | 9f394a16c557 |
| 61142:6d29eb7c5fb2 | 61143:5f898411ce87 |
|---|---|
2 theory Reference |
2 theory Reference |
3 imports "../SPARK" |
3 imports "../SPARK" |
4 begin |
4 begin |
5 |
5 |
6 syntax (my_constrain output) |
6 syntax (my_constrain output) |
7 "_constrain" :: "logic => type => logic" ("_ \<Colon> _" [4, 0] 3) |
7 "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3) |
8 (*>*) |
8 (*>*) |
9 |
9 |
10 chapter {* HOL-\SPARK{} Reference *} |
10 chapter {* HOL-\SPARK{} Reference *} |
11 |
11 |
12 text {* |
12 text {* |