equal
deleted
inserted
replaced
59 subsection \<open>Properties\<close> |
59 subsection \<open>Properties\<close> |
60 |
60 |
61 text \<open>Primitives\<close> |
61 text \<open>Primitives\<close> |
62 |
62 |
63 lemma noteq_sym: "r =!= s \<Longrightarrow> s =!= r" |
63 lemma noteq_sym: "r =!= s \<Longrightarrow> s =!= r" |
64 and unequal [simp]: "r \<noteq> r' \<longleftrightarrow> r =!= r'" \<comment> "same types!" |
64 and unequal [simp]: "r \<noteq> r' \<longleftrightarrow> r =!= r'" \<comment> \<open>same types!\<close> |
65 by (auto simp add: noteq_def) |
65 by (auto simp add: noteq_def) |
66 |
66 |
67 lemma noteq_irrefl: "r =!= r \<Longrightarrow> False" |
67 lemma noteq_irrefl: "r =!= r \<Longrightarrow> False" |
68 by (auto simp add: noteq_def) |
68 by (auto simp add: noteq_def) |
69 |
69 |