equal
deleted
inserted
replaced
97 |
97 |
98 |
98 |
99 types vvar = "val \<times> (val \<Rightarrow> state \<Rightarrow> state)" |
99 types vvar = "val \<times> (val \<Rightarrow> state \<Rightarrow> state)" |
100 vals = "(val, vvar, val list) sum3" |
100 vals = "(val, vvar, val list) sum3" |
101 translations |
101 translations |
102 "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)" |
102 (type) "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)" |
103 "vals" <= (type)"(val, vvar, val list) sum3" |
103 (type) "vals" <= (type) "(val, vvar, val list) sum3" |
104 |
104 |
105 text {* To avoid redundancy and to reduce the number of rules, there is only |
105 text {* To avoid redundancy and to reduce the number of rules, there is only |
106 one evaluation rule for each syntactic term. This is also true for variables |
106 one evaluation rule for each syntactic term. This is also true for variables |
107 (e.g. see the rules below for @{text LVar}, @{text FVar} and @{text AVar}). |
107 (e.g. see the rules below for @{text LVar}, @{text FVar} and @{text AVar}). |
108 So evaluation of a variable must capture both possible further uses: |
108 So evaluation of a variable must capture both possible further uses: |