equal
deleted
inserted
replaced
94 "assign" :: "[i,i,i] => i" ("_[_'/_]" [95,0,0] 95) |
94 "assign" :: "[i,i,i] => i" ("_[_'/_]" [95,0,0] 95) |
95 |
95 |
96 translations |
96 translations |
97 "<ce,sig> -c-> s" == "<ce,sig,s> : evalc" |
97 "<ce,sig> -c-> s" == "<ce,sig,s> : evalc" |
98 |
98 |
99 rules |
99 defs |
100 assign_def "sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)" |
100 assign_def "sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)" |
101 |
101 |
102 inductive |
102 inductive |
103 domains "evalc" <= "com * (loc -> nat) * (loc -> nat)" |
103 domains "evalc" <= "com * (loc -> nat) * (loc -> nat)" |
104 intrs |
104 intrs |