Quot/Examples/FSet3.thy
changeset 796 64f9c76f70c7
parent 794 f0a78fda343f
child 797 35436401f00d
--- 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