src/HOL/IMP/Def_Ass.thy
changeset 45212 e87feee00a4c
parent 43158 686fa0a0696e
child 47818 151d137f1095
     1.1 --- a/src/HOL/IMP/Def_Ass.thy	Wed Oct 19 23:07:48 2011 +0200
     1.2 +++ b/src/HOL/IMP/Def_Ass.thy	Thu Oct 20 09:48:00 2011 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4  
     1.5  subsection "Definite Assignment Analysis"
     1.6  
     1.7 -inductive D :: "name set \<Rightarrow> com \<Rightarrow> name set \<Rightarrow> bool" where
     1.8 +inductive D :: "vname set \<Rightarrow> com \<Rightarrow> vname set \<Rightarrow> bool" where
     1.9  Skip: "D A SKIP A" |
    1.10  Assign: "vars a \<subseteq> A \<Longrightarrow> D A (x ::= a) (insert x A)" |
    1.11  Semi: "\<lbrakk> D A\<^isub>1 c\<^isub>1 A\<^isub>2;  D A\<^isub>2 c\<^isub>2 A\<^isub>3 \<rbrakk> \<Longrightarrow> D A\<^isub>1 (c\<^isub>1; c\<^isub>2) A\<^isub>3" |