changeset 1401 | 0c439768f45c |
parent 1155 | 928a16e02f9f |
child 1478 | 2b8c2a7547ab |
1400:5d909faf0e04 | 1401:0c439768f45c |
---|---|
5 *) |
5 *) |
6 |
6 |
7 Dynamic = Values + |
7 Dynamic = Values + |
8 |
8 |
9 consts |
9 consts |
10 EvalRel :: "i" |
10 EvalRel :: i |
11 inductive |
11 inductive |
12 domains "EvalRel" <= "ValEnv * Exp * Val" |
12 domains "EvalRel" <= "ValEnv * Exp * Val" |
13 intrs |
13 intrs |
14 eval_constI |
14 eval_constI |
15 " [| ve:ValEnv; c:Const |] ==> |
15 " [| ve:ValEnv; c:Const |] ==> |