doc-src/TutorialI/Sets/Relations.thy
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