| changeset 61143 | 5f898411ce87 |
| parent 59938 | f84b93187ab6 |
| child 62969 | 9f394a16c557 |
--- a/src/HOL/SPARK/Manual/Reference.thy Wed Sep 09 11:24:34 2015 +0200 +++ b/src/HOL/SPARK/Manual/Reference.thy Wed Sep 09 14:47:41 2015 +0200 @@ -4,7 +4,7 @@ begin syntax (my_constrain output) - "_constrain" :: "logic => type => logic" ("_ \<Colon> _" [4, 0] 3) + "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3) (*>*) chapter {* HOL-\SPARK{} Reference *}