src/ZF/UNITY/Mutex.thy
changeset 67445 4311845b0412
parent 67443 3abf6a722518
equal deleted inserted replaced
67444:100247708f31 67445:4311845b0412
    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"