diff -r d027515e2aa6 -r 04b0e943fcc9 src/HOL/UNITY/Transformers.thy
--- a/src/HOL/UNITY/Transformers.thy	Mon Aug 02 16:06:13 2004 +0200
+++ b/src/HOL/UNITY/Transformers.thy	Tue Aug 03 13:48:00 2004 +0200
@@ -121,6 +121,10 @@
 text{*Assertion 4.17 in the thesis*}
 lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A" 
 by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
+  --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
+      is declared as an iff-rule, then it's almost impossible to prove. 
+      One proof is via @{text meson} after expanding all definitions, but it's
+      slow!*}
 
 text{*Assertion (7): 4.18 in the thesis.  NOTE that many of these results
 hold for an arbitrary action.  We often do not require @{term "act \<in> Acts F"}*}