equal
deleted
inserted
replaced
60 subsection{*Definitions*} |
60 subsection{*Definitions*} |
61 |
61 |
62 consts xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" |
62 consts xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" |
63 defs xor_def: "xor x y \<equiv> x \<and> \<not>y \<or> \<not>x \<and> y" |
63 defs xor_def: "xor x y \<equiv> x \<and> \<not>y \<or> \<not>x \<and> y" |
64 |
64 |
65 constdefs nand :: "bool \<Rightarrow> bool \<Rightarrow> bool" |
65 definition nand :: "bool \<Rightarrow> bool \<Rightarrow> bool" where |
66 "nand x y \<equiv> \<not>(x \<and> y)" |
66 "nand x y \<equiv> \<not>(x \<and> y)" |
67 |
67 |
68 lemma "\<not> xor x x" |
68 lemma "\<not> xor x x" |
69 apply(unfold xor_def) |
69 apply(unfold xor_def) |
70 by auto |
70 by auto |