changeset 26806 | 40b411ec05aa |
parent 16417 | 9bc16273c2d4 |
child 36754 | 403585a89772 |
1.1 --- a/doc-src/TutorialI/Sets/Relations.thy Wed May 07 10:56:58 2008 +0200 1.2 +++ b/doc-src/TutorialI/Sets/Relations.thy Wed May 07 10:57:19 2008 +0200 1.3 @@ -151,7 +151,7 @@ 1.4 text{*Pow, Inter too little used*} 1.5 1.6 lemma "(A \<subset> B) = (A \<subseteq> B \<and> A \<noteq> B)" 1.7 -apply (simp add: psubset_def) 1.8 +apply (simp add: psubset_eq) 1.9 done 1.10 1.11 end