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