--- a/Quot/Examples/FSet3.thy Sat Dec 26 21:36:20 2009 +0100 +++ b/Quot/Examples/FSet3.thy Sat Dec 26 23:20:46 2009 +0100 @@ -600,5 +600,7 @@ apply (lifting list.cases(2)) done +thm quot_respect + end