| changeset 62020 | 5d208fd2507d |
| parent 60770 | 240563fbf41d |
| child 62143 | 3c9a0985e6be |
--- a/src/CCL/Set.thy Thu Dec 31 21:46:31 2015 +0100 +++ b/src/CCL/Set.thy Fri Jan 01 10:49:00 2016 +0100 @@ -411,7 +411,7 @@ by (blast intro: equalityI elim: equalityE) -subsection \<open>Simple properties of @{text "Compl"} -- complement of a set\<close> +subsection \<open>Simple properties of \<open>Compl\<close> -- complement of a set\<close> lemma Compl_disjoint: "A Int Compl(A) = {x. False}" by (blast intro: equalityI)