changeset 66992 | 69673025292e |
parent 66453 | cc19f7ca2ed6 |
child 69597 | ff784d5a5bfb |
66991:fc87d3becd69 | 66992:69673025292e |
---|---|
1 (*<*) |
1 (*<*) |
2 theory Reference |
2 theory Reference |
3 imports SPARK |
3 imports "HOL-SPARK.SPARK" |
4 begin |
4 begin |
5 |
5 |
6 syntax (my_constrain output) |
6 syntax (my_constrain output) |
7 "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3) |
7 "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3) |
8 (*>*) |
8 (*>*) |