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 *}