equal
deleted
inserted
replaced
70 |
70 |
71 instantiation com :: vars |
71 instantiation com :: vars |
72 begin |
72 begin |
73 |
73 |
74 fun vars_com :: "com \<Rightarrow> vname set" where |
74 fun vars_com :: "com \<Rightarrow> vname set" where |
75 "vars com.SKIP = {}" | |
75 "vars SKIP = {}" | |
76 "vars (x::=e) = {x} \<union> vars e" | |
76 "vars (x::=e) = {x} \<union> vars e" | |
77 "vars (c1;c2) = vars c1 \<union> vars c2" | |
77 "vars (c1;;c2) = vars c1 \<union> vars c2" | |
78 "vars (IF b THEN c1 ELSE c2) = vars b \<union> vars c1 \<union> vars c2" | |
78 "vars (IF b THEN c1 ELSE c2) = vars b \<union> vars c1 \<union> vars c2" | |
79 "vars (WHILE b DO c) = vars b \<union> vars c" |
79 "vars (WHILE b DO c) = vars b \<union> vars c" |
80 |
80 |
81 instance .. |
81 instance .. |
82 |
82 |