src/ZF/UNITY/Mutex.thy
changeset 67443 3abf6a722518
parent 67399 eab6ce8368fa
child 67445 4311845b0412
equal deleted inserted replaced
67442:f075640b8868 67443:3abf6a722518
    25 abbreviation "m == Var([1])"
    25 abbreviation "m == Var([1])"
    26 abbreviation "n == Var([0,0])"
    26 abbreviation "n == Var([0,0])"
    27 abbreviation "u == Var([0,1])"
    27 abbreviation "u == Var([0,1])"
    28 abbreviation "v == Var([1,0])"
    28 abbreviation "v == Var([1,0])"
    29 
    29 
    30 axiomatization where \<comment>\<open>* Type declarations  *\<close>
    30 axiomatization where \<comment> \<open>* Type declarations  *\<close>
    31   p_type:  "type_of(p)=bool & default_val(p)=0" and
    31   p_type:  "type_of(p)=bool & default_val(p)=0" and
    32   m_type:  "type_of(m)=int  & default_val(m)=#0" and
    32   m_type:  "type_of(m)=int  & default_val(m)=#0" and
    33   n_type:  "type_of(n)=int  & default_val(n)=#0" and
    33   n_type:  "type_of(n)=int  & default_val(n)=#0" and
    34   u_type:  "type_of(u)=bool & default_val(u)=0" and
    34   u_type:  "type_of(u)=bool & default_val(u)=0" and
    35   v_type:  "type_of(v)=bool & default_val(v)=0"
    35   v_type:  "type_of(v)=bool & default_val(v)=0"