changeset 1401 | 0c439768f45c |
parent 1155 | 928a16e02f9f |
child 1478 | 2b8c2a7547ab |
1400:5d909faf0e04 | 1401:0c439768f45c |
---|---|
5 *) |
5 *) |
6 |
6 |
7 Static = BCR + |
7 Static = BCR + |
8 |
8 |
9 consts |
9 consts |
10 ElabRel :: "i" |
10 ElabRel :: i |
11 inductive |
11 inductive |
12 domains "ElabRel" <= "TyEnv * Exp * Ty" |
12 domains "ElabRel" <= "TyEnv * Exp * Ty" |
13 intrs |
13 intrs |
14 elab_constI |
14 elab_constI |
15 " [| te:TyEnv; c:Const; t:Ty; isof(c,t) |] ==> |
15 " [| te:TyEnv; c:Const; t:Ty; isof(c,t) |] ==> |