equal
deleted
inserted
replaced
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" |