src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy
changeset 45827 66c68453455c
parent 42795 66fcc9882784
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Tue Dec 13 14:04:20 2011 +0100
     1.2 +++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Tue Dec 13 15:18:52 2011 +0100
     1.3 @@ -380,13 +380,12 @@
     1.4  
     1.5  subsubsection {* Appending garbage nodes to the free list *}
     1.6  
     1.7 -consts  Append_to_free :: "nat \<times> edges \<Rightarrow> edges"
     1.8 -
     1.9 -axioms
    1.10 -  Append_to_free0: "length (Append_to_free (i, e)) = length e"
    1.11 -  Append_to_free1: "Proper_Edges (m, e) 
    1.12 -                    \<Longrightarrow> Proper_Edges (m, Append_to_free(i, e))"
    1.13 -  Append_to_free2: "i \<notin> Reach e 
    1.14 +axiomatization Append_to_free :: "nat \<times> edges \<Rightarrow> edges"
    1.15 +where
    1.16 +  Append_to_free0: "length (Append_to_free (i, e)) = length e" and
    1.17 +  Append_to_free1: "Proper_Edges (m, e)
    1.18 +                    \<Longrightarrow> Proper_Edges (m, Append_to_free(i, e))" and
    1.19 +  Append_to_free2: "i \<notin> Reach e
    1.20             \<Longrightarrow> n \<in> Reach (Append_to_free(i, e)) = ( n = i \<or> n \<in> Reach e)"
    1.21  
    1.22  definition Mul_AppendInv :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where