changeset 58130 | 5e9170812356 |
parent 56798 | 939e88e79724 |
child 59938 | f84b93187ab6 |
58129:3ec65a7f2b50 | 58130:5e9170812356 |
---|---|
1 (*<*) |
1 (*<*) |
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" ("_ \<Colon> _" [4, 0] 3) |
8 (*>*) |
8 (*>*) |