# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1287145719 -3600
# Node ID 22c37deb3dacbfac486d40d1967ae787ac7ebb5a
# Parent  8054f4988672891a463f679db4ddec01854fa0e7
typo

diff -r 8054f4988672 -r 22c37deb3dac Nominal/FSet.thy
--- a/Nominal/FSet.thy	Fri Oct 15 16:32:34 2010 +0900
+++ b/Nominal/FSet.thy	Fri Oct 15 13:28:39 2010 +0100
@@ -160,7 +160,7 @@
   by (induct ys arbitrary: xs) (auto)
 
 
-text {* Respectfullness *}
+text {* Respectfulness *}
 
 lemma append_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
@@ -299,7 +299,7 @@
 qed
 
 lemma [quot_respect]:
-  shows "((op =) ===> op \<approx> ===> op \<approx>) filter filter"
+  shows "(op = ===> op \<approx> ===> op \<approx>) filter filter"
   by auto
 
 text {* Distributive lattice with bot *}