diff options
| -rw-r--r-- | docs/core-spec/CoreLint.ott | 4 | ||||
| -rw-r--r-- | docs/core-spec/CoreSyn.ott | 2 | ||||
| -rw-r--r-- | docs/core-spec/core-spec.pdf | bin | 339274 -> 339243 bytes |
3 files changed, 4 insertions, 2 deletions
diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott index 4c51a0559a..56b4b99151 100644 --- a/docs/core-spec/CoreLint.ott +++ b/docs/core-spec/CoreLint.ott @@ -247,7 +247,7 @@ G |-co g t0 : s[m |-> t0] ~R k t[n |-> t0] C = T_R0 </ axBranchkk // kk /> 0 <= ind < length </ axBranchkk // kk /> -forall </ ni_Ri // i />. (</ s1j // j /> ~> t1) = (</ axBranchkk // kk />)[ind] +forall </ ni_^^Ri // i />. (</ s1j // j /> ~> t1) = (</ axBranchkk // kk />)[ind] </ G |-co gi : s'i ~Ri k'i t'i // i /> </ substi @ // i /> = inits(</ [ ni |-> s'i ] // i />) </ ni = zi_ki // i /> @@ -536,4 +536,4 @@ forall </ n'i_R'i // i />. (</ t'j // j /> ~> s') = (</ axBranchkk // kk />)[ind unify(</ tj // j />, </ t'j // j />) = subst subst(s) = subst(s') ----------------------------------------- :: CompatCoincident -no_conflict(C, </ sj // j />, ind1, ind2)
\ No newline at end of file +no_conflict(C, </ sj // j />, ind1, ind2) diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott index 56594eca26..0c5b30483e 100644 --- a/docs/core-spec/CoreSyn.ott +++ b/docs/core-spec/CoreSyn.ott @@ -235,6 +235,8 @@ type_list :: 'TypeList_' ::= {{ com List of types }} RA {{ tex {\!\!\!{}_{\rho} } }} :: 'RoleAnnot_' ::= {{ com Role annotation }} | _ R :: M :: annotation {{ tex {\!\!\!{}_{[[R]]} } }} + | _ ^^ R :: M :: spaced_annotation + {{ tex {}_{[[R]]} }} role_list {{ tex {\overline{\rho_j} }^j }} :: 'RoleList_' ::= {{ com List of roles }} | </ Ri // , // i /> :: :: List diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf Binary files differindex 5d9f29c58b..52f2e39f83 100644 --- a/docs/core-spec/core-spec.pdf +++ b/docs/core-spec/core-spec.pdf |