Quot/Examples/FSet3.thy
changeset 854 5961edda27d7
parent 833 129caba33c03
child 856 433f7c17255f
--- a/Quot/Examples/FSet3.thy	Tue Jan 12 10:59:51 2010 +0100
+++ b/Quot/Examples/FSet3.thy	Wed Jan 13 00:45:28 2010 +0100
@@ -369,8 +369,6 @@
 apply(cleaning)
 apply (simp add: finsert_def fconcat_def comp_def)
 apply cleaning
-(* ID PROBLEM *)
-apply(simp add: id_def[symmetric] id_simps)
 done
 
 text {* raw section *}