# HG changeset patch
# User nipkow
# Date 1253277624 -7200
# Node ID c0056c2c1d17dff5c2231537ca51d25399e8f168
# Parent  b5c3a8a7577245b91aa805e57c327fef1ed93088# Parent  e7fe01b74a9200f24f65c31771c1b19cb25e48d7
merged

diff -r e7fe01b74a92 -r c0056c2c1d17 CONTRIBUTORS
--- a/CONTRIBUTORS	Fri Sep 18 14:40:06 2009 +0200
+++ b/CONTRIBUTORS	Fri Sep 18 14:40:24 2009 +0200
@@ -7,6 +7,12 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* September 2009: Florian Haftmann, TUM
+  Refinement of Sets and Lattices
+
+* July 2009: Jeremy Avigad and Amine Chaieb
+  New number theory
+
 * July 2009: Philipp Meyer, TUM
   HOL/Library/Sum_of_Squares: functionality to call a remote csdp prover
 
diff -r e7fe01b74a92 -r c0056c2c1d17 NEWS
--- a/NEWS	Fri Sep 18 14:40:06 2009 +0200
+++ b/NEWS	Fri Sep 18 14:40:24 2009 +0200
@@ -19,14 +19,28 @@
 *** HOL ***
 
 * Reorganization of number theory:
-  * former session NumberTheory now named Old_Number_Theory; former session NewNumberTheory
-    named NumberTheory;
-  * split off prime number ingredients from theory GCD to theory Number_Theory/Primes;
+  * former session NumberTheory now named Old_Number_Theory
+  * new session Number_Theory by Jeremy Avigad; if possible, prefer this.
   * moved legacy theories Legacy_GCD and Primes from Library/ to Old_Number_Theory/;
   * moved theory Pocklington from Library/ to Old_Number_Theory/;
   * removed various references to Old_Number_Theory from HOL distribution.
 INCOMPATIBILITY.
 
+* Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm
+of finite and infinite sets. It is shown that they form a complete
+lattice.
+
+* Split off prime number ingredients from theory GCD
+to theory Number_Theory/Primes;
+
+* Class semiring_div requires superclass no_zero_divisors and proof of
+div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
+div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
+generalized to class semiring_div, subsuming former theorems
+zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
+zdiv_zmult_zmult2.  div_mult_mult1 is now [simp] by default.
+INCOMPATIBILITY.
+
 * New testing tool "Mirabelle" for automated (proof) tools. Applies
 several tools and tactics like sledgehammer, metis, or quickcheck, to
 every proof step in a theory. To be used in batch mode via the
@@ -47,16 +61,15 @@
     etc.
   INCOMPATIBILITY.
 
-* New class "boolean_algebra".
-
 * Refinements to lattice classes and sets:
   - less default intro/elim rules in locale variant, more default
     intro/elim rules in class variant: more uniformity
   - lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff
   - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci)
   - renamed ACI to inf_sup_aci
+  - new class "boolean_algebra"
   - class "complete_lattice" moved to separate theory "complete_lattice";
-    corresponding constants (and abbreviations) renamed:
+    corresponding constants (and abbreviations) renamed and with authentic syntax:
     Set.Inf ~>      Complete_Lattice.Inf
     Set.Sup ~>      Complete_Lattice.Sup
     Set.INFI ~>     Complete_Lattice.INFI
@@ -66,24 +79,22 @@
     Set.INTER ~>    Complete_Lattice.INTER
     Set.UNION ~>    Complete_Lattice.UNION
   - more convenient names for set intersection and union:
-    Set.Int ~>  Set.inter
-    Set.Un ~>   Set.union
+    Set.Int ~>      Set.inter
+    Set.Un ~>       Set.union
+  - authentic syntax for
+    Set.Pow
+    Set.image
   - mere abbreviations:
     Set.empty               (for bot)
     Set.UNIV                (for top)
     Complete_Lattice.Inter  (for Inf)
     Complete_Lattice.Union  (for Sup)
+    Complete_Lattice.INTER  (for INFI)
+    Complete_Lattice.UNION  (for SUPR)
+  - object-logic definitions as far as appropriate
 
   INCOMPATIBILITY.
 
-* Class semiring_div requires superclass no_zero_divisors and proof of
-div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
-div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
-generalized to class semiring_div, subsuming former theorems
-zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
-zdiv_zmult_zmult2.  div_mult_mult1 is now [simp] by default.
-INCOMPATIBILITY.
-
 * Power operations on relations and functions are now one dedicate
 constant "compow" with infix syntax "^^".  Power operations on
 multiplicative monoids retains syntax "^" and is now defined generic
@@ -96,10 +107,6 @@
 this.  Fix using O_assoc[symmetric].  The same applies to the curried
 version "R OO S".
 
-* Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm
-of finite and infinite sets. It is shown that they form a complete
-lattice.
-
 * ML antiquotation @{code_datatype} inserts definition of a datatype
 generated by the code generator; see Predicate.thy for an example.
 
@@ -110,10 +117,6 @@
 default generators are provided for all suitable HOL types, records
 and datatypes.
 
-* Constants Set.Pow and Set.image now with authentic syntax;
-object-logic definitions Set.Pow_def and Set.image_def.
-INCOMPATIBILITY.
-
 * Renamed theorems:
 Suc_eq_add_numeral_1 -> Suc_eq_plus1
 Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
@@ -138,9 +141,6 @@
 
 INCOMPATIBILITY.
 
-* NewNumberTheory: Jeremy Avigad's new version of part of
-NumberTheory.  If possible, use NewNumberTheory, not NumberTheory.
-
 * Discontinued abbreviation "arbitrary" of constant
 "undefined". INCOMPATIBILITY, use "undefined" directly.
 
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Complete_Lattice.thy	Fri Sep 18 14:40:24 2009 +0200
@@ -278,8 +278,8 @@
 
 subsection {* Unions of families *}
 
-definition UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
-  SUPR_set_eq [symmetric]: "UNION S f = (SUP x:S. f x)"
+abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
+  "UNION \<equiv> SUPR"
 
 syntax
   "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
@@ -314,7 +314,7 @@
 
 lemma UNION_eq_Union_image:
   "(\<Union>x\<in>A. B x) = \<Union>(B`A)"
-  by (simp add: SUPR_def SUPR_set_eq [symmetric])
+  by (fact SUPR_def)
 
 lemma Union_def:
   "\<Union>S = (\<Union>x\<in>S. x)"
@@ -351,7 +351,7 @@
   by blast
 
 lemma UN_upper: "a \<in> A ==> B a \<subseteq> (\<Union>x\<in>A. B x)"
-  by blast
+  by (fact le_SUPI)
 
 lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"
   by (iprover intro: subsetI elim: UN_E dest: subsetD)
@@ -514,8 +514,8 @@
 
 subsection {* Intersections of families *}
 
-definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
-  INFI_set_eq [symmetric]: "INTER S f = (INF x:S. f x)"
+abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
+  "INTER \<equiv> INFI"
 
 syntax
   "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
@@ -541,7 +541,7 @@
 
 lemma INTER_eq_Inter_image:
   "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
-  by (simp add: INFI_def INFI_set_eq [symmetric])
+  by (fact INFI_def)
   
 lemma Inter_def:
   "\<Inter>S = (\<Inter>x\<in>S. x)"
@@ -579,10 +579,10 @@
   by blast
 
 lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a"
-  by blast
+  by (fact INF_leI)
 
 lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)"
-  by (iprover intro: INT_I subsetI dest: subsetD)
+  by (fact le_INFI)
 
 lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
   by blast
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Lambda/Eta.thy	Fri Sep 18 14:40:24 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Lambda/Eta.thy
-    ID:         $Id$
     Author:     Tobias Nipkow and Stefan Berghofer
     Copyright   1995, 2005 TU Muenchen
 *)
@@ -87,7 +86,6 @@
 lemma square_eta: "square eta eta (eta^==) (eta^==)"
   apply (unfold square_def id_def)
   apply (rule impI [THEN allI [THEN allI]])
-  apply simp
   apply (erule eta.induct)
      apply (slowsimp intro: subst_not_free eta_subst free_eta [THEN iffD1])
     apply safe
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Fri Sep 18 14:40:24 2009 +0200
@@ -32,8 +32,8 @@
 
 declare inter [code]
 
-declare Inter_image_eq [symmetric, code]
-declare Union_image_eq [symmetric, code]
+declare Inter_image_eq [symmetric, code_unfold]
+declare Union_image_eq [symmetric, code_unfold]
 
 declare List_Set.project_def [symmetric, code_unfold]
 
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Predicate.thy	Fri Sep 18 14:40:24 2009 +0200
@@ -75,29 +75,29 @@
 
 subsubsection {* Binary union *}
 
-lemma sup1_iff [simp]: "sup A B x \<longleftrightarrow> A x | B x"
+lemma sup1_iff: "sup A B x \<longleftrightarrow> A x | B x"
   by (simp add: sup_fun_eq sup_bool_eq)
 
-lemma sup2_iff [simp]: "sup A B x y \<longleftrightarrow> A x y | B x y"
+lemma sup2_iff: "sup A B x y \<longleftrightarrow> A x y | B x y"
   by (simp add: sup_fun_eq sup_bool_eq)
 
 lemma sup_Un_eq [pred_set_conv]: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
-  by (simp add: expand_fun_eq)
+  by (simp add: sup1_iff expand_fun_eq)
 
 lemma sup_Un_eq2 [pred_set_conv]: "sup (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
-  by (simp add: expand_fun_eq)
+  by (simp add: sup2_iff expand_fun_eq)
 
 lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x"
-  by simp
+  by (simp add: sup1_iff)
 
 lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y"
-  by simp
+  by (simp add: sup2_iff)
 
 lemma sup1I2 [elim?]: "B x \<Longrightarrow> sup A B x"
-  by simp
+  by (simp add: sup1_iff)
 
 lemma sup2I2 [elim?]: "B x y \<Longrightarrow> sup A B x y"
-  by simp
+  by (simp add: sup2_iff)
 
 text {*
   \medskip Classical introduction rule: no commitment to @{text A} vs
@@ -105,115 +105,115 @@
 *}
 
 lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x"
-  by auto
+  by (auto simp add: sup1_iff)
 
 lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y"
-  by auto
+  by (auto simp add: sup2_iff)
 
 lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
-  by simp iprover
+  by (simp add: sup1_iff) iprover
 
 lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
-  by simp iprover
+  by (simp add: sup2_iff) iprover
 
 
 subsubsection {* Binary intersection *}
 
-lemma inf1_iff [simp]: "inf A B x \<longleftrightarrow> A x \<and> B x"
+lemma inf1_iff: "inf A B x \<longleftrightarrow> A x \<and> B x"
   by (simp add: inf_fun_eq inf_bool_eq)
 
-lemma inf2_iff [simp]: "inf A B x y \<longleftrightarrow> A x y \<and> B x y"
+lemma inf2_iff: "inf A B x y \<longleftrightarrow> A x y \<and> B x y"
   by (simp add: inf_fun_eq inf_bool_eq)
 
 lemma inf_Int_eq [pred_set_conv]: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
-  by (simp add: expand_fun_eq)
+  by (simp add: inf1_iff expand_fun_eq)
 
 lemma inf_Int_eq2 [pred_set_conv]: "inf (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
-  by (simp add: expand_fun_eq)
+  by (simp add: inf2_iff expand_fun_eq)
 
 lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
-  by simp
+  by (simp add: inf1_iff)
 
 lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
-  by simp
+  by (simp add: inf2_iff)
 
 lemma inf1D1: "inf A B x ==> A x"
-  by simp
+  by (simp add: inf1_iff)
 
 lemma inf2D1: "inf A B x y ==> A x y"
-  by simp
+  by (simp add: inf2_iff)
 
 lemma inf1D2: "inf A B x ==> B x"
-  by simp
+  by (simp add: inf1_iff)
 
 lemma inf2D2: "inf A B x y ==> B x y"
-  by simp
+  by (simp add: inf2_iff)
 
 lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
-  by simp
+  by (simp add: inf1_iff)
 
 lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
-  by simp
+  by (simp add: inf2_iff)
 
 
 subsubsection {* Unions of families *}
 
-lemma SUP1_iff [simp]: "(SUP x:A. B x) b = (EX x:A. B x b)"
+lemma SUP1_iff: "(SUP x:A. B x) b = (EX x:A. B x b)"
   by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
 
-lemma SUP2_iff [simp]: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
+lemma SUP2_iff: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
   by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
 
 lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b"
-  by auto
+  by (auto simp add: SUP1_iff)
 
 lemma SUP2_I [intro]: "a : A ==> B a b c ==> (SUP x:A. B x) b c"
-  by auto
+  by (auto simp add: SUP2_iff)
 
 lemma SUP1_E [elim!]: "(SUP x:A. B x) b ==> (!!x. x : A ==> B x b ==> R) ==> R"
-  by auto
+  by (auto simp add: SUP1_iff)
 
 lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R"
-  by auto
+  by (auto simp add: SUP2_iff)
 
 lemma SUP_UN_eq: "(SUP i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (UN i. r i))"
-  by (simp add: expand_fun_eq)
+  by (simp add: SUP1_iff expand_fun_eq)
 
 lemma SUP_UN_eq2: "(SUP i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (UN i. r i))"
-  by (simp add: expand_fun_eq)
+  by (simp add: SUP2_iff expand_fun_eq)
 
 
 subsubsection {* Intersections of families *}
 
-lemma INF1_iff [simp]: "(INF x:A. B x) b = (ALL x:A. B x b)"
+lemma INF1_iff: "(INF x:A. B x) b = (ALL x:A. B x b)"
   by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
 
-lemma INF2_iff [simp]: "(INF x:A. B x) b c = (ALL x:A. B x b c)"
+lemma INF2_iff: "(INF x:A. B x) b c = (ALL x:A. B x b c)"
   by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
 
 lemma INF1_I [intro!]: "(!!x. x : A ==> B x b) ==> (INF x:A. B x) b"
-  by auto
+  by (auto simp add: INF1_iff)
 
 lemma INF2_I [intro!]: "(!!x. x : A ==> B x b c) ==> (INF x:A. B x) b c"
-  by auto
+  by (auto simp add: INF2_iff)
 
 lemma INF1_D [elim]: "(INF x:A. B x) b ==> a : A ==> B a b"
-  by auto
+  by (auto simp add: INF1_iff)
 
 lemma INF2_D [elim]: "(INF x:A. B x) b c ==> a : A ==> B a b c"
-  by auto
+  by (auto simp add: INF2_iff)
 
 lemma INF1_E [elim]: "(INF x:A. B x) b ==> (B a b ==> R) ==> (a ~: A ==> R) ==> R"
-  by auto
+  by (auto simp add: INF1_iff)
 
 lemma INF2_E [elim]: "(INF x:A. B x) b c ==> (B a b c ==> R) ==> (a ~: A ==> R) ==> R"
-  by auto
+  by (auto simp add: INF2_iff)
 
 lemma INF_INT_eq: "(INF i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (INT i. r i))"
-  by (simp add: expand_fun_eq)
+  by (simp add: INF1_iff expand_fun_eq)
 
 lemma INF_INT_eq2: "(INF i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (INT i. r i))"
-  by (simp add: expand_fun_eq)
+  by (simp add: INF2_iff expand_fun_eq)
 
 
 subsection {* Predicates as relations *}
@@ -429,7 +429,7 @@
   by (auto simp add: bind_def sup_pred_def expand_fun_eq)
 
 lemma Sup_bind: "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
-  by (auto simp add: bind_def Sup_pred_def expand_fun_eq)
+  by (auto simp add: bind_def Sup_pred_def SUP1_iff expand_fun_eq)
 
 lemma pred_iffI:
   assumes "\<And>x. eval A x \<Longrightarrow> eval B x"
@@ -462,10 +462,10 @@
   unfolding bot_pred_def by auto
 
 lemma supI1: "eval A x \<Longrightarrow> eval (A \<squnion> B) x"
-  unfolding sup_pred_def by simp
+  unfolding sup_pred_def by (simp add: sup1_iff)
 
 lemma supI2: "eval B x \<Longrightarrow> eval (A \<squnion> B) x" 
-  unfolding sup_pred_def by simp
+  unfolding sup_pred_def by (simp add: sup1_iff)
 
 lemma supE: "eval (A \<squnion> B) x \<Longrightarrow> (eval A x \<Longrightarrow> P) \<Longrightarrow> (eval B x \<Longrightarrow> P) \<Longrightarrow> P"
   unfolding sup_pred_def by auto
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Tools/Function/decompose.ML
--- a/src/HOL/Tools/Function/decompose.ML	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Function/decompose.ML	Fri Sep 18 14:40:24 2009 +0200
@@ -29,7 +29,7 @@
       fun prove_chain c1 c2 D =
           if is_some (Termination.get_chain D c1 c2) then D else
           let
-            val goal = HOLogic.mk_eq (HOLogic.mk_binop @{const_name "Relation.rel_comp"} (c1, c2),
+            val goal = HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.rel_comp} (c1, c2),
                                       Const (@{const_name Set.empty}, fastype_of c1))
                        |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
 
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Tools/Function/fundef_common.ML
--- a/src/HOL/Tools/Function/fundef_common.ML	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_common.ML	Fri Sep 18 14:40:24 2009 +0200
@@ -16,7 +16,7 @@
 fun PROFILE msg = if !profile then timeap_msg msg else I
 
 
-val acc_const_name = @{const_name "accp"}
+val acc_const_name = @{const_name accp}
 fun mk_acc domT R =
     Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
 
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Tools/Function/fundef_core.ML
--- a/src/HOL/Tools/Function/fundef_core.ML	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_core.ML	Fri Sep 18 14:40:24 2009 +0200
@@ -769,7 +769,7 @@
       val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
       val inrel_R = Const (@{const_name FunDef.in_rel}, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
 
-      val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name "Wellfounded.wfP"}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
+      val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
 
       (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
       val ihyp = Term.all domT $ Abs ("z", domT,
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Tools/Function/induction_scheme.ML
--- a/src/HOL/Tools/Function/induction_scheme.ML	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Function/induction_scheme.ML	Fri Sep 18 14:40:24 2009 +0200
@@ -152,7 +152,7 @@
     end
 
 fun mk_wf ctxt R (IndScheme {T, ...}) =
-    HOLogic.Trueprop $ (Const (@{const_name "wf"}, mk_relT T --> HOLogic.boolT) $ R)
+    HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
 
 fun mk_ineqs R (IndScheme {T, cases, branches}) =
     let
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Fri Sep 18 14:40:24 2009 +0200
@@ -26,7 +26,7 @@
         val mlexT = (domT --> HOLogic.natT) --> relT --> relT
         fun mk_ms [] = Const (@{const_name Set.empty}, relT)
           | mk_ms (f::fs) = 
-            Const (@{const_name "mlex_prod"}, mlexT) $ f $ mk_ms fs
+            Const (@{const_name mlex_prod}, mlexT) $ f $ mk_ms fs
     in
         mk_ms mfuns
     end
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Tools/Function/measure_functions.ML
--- a/src/HOL/Tools/Function/measure_functions.ML	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Function/measure_functions.ML	Fri Sep 18 14:40:24 2009 +0200
@@ -22,7 +22,7 @@
   val description = "Rules that guide the heuristic generation of measure functions"
 );
 
-fun mk_is_measures t = Const (@{const_name "is_measure"}, fastype_of t --> HOLogic.boolT) $ t
+fun mk_is_measures t = Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t
 
 fun find_measures ctxt T =
   DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1) 
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Tools/Function/sum_tree.ML
--- a/src/HOL/Tools/Function/sum_tree.ML	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Function/sum_tree.ML	Fri Sep 18 14:40:24 2009 +0200
@@ -17,22 +17,22 @@
 
 (* Sum types *)
 fun mk_sumT LT RT = Type ("+", [LT, RT])
-fun mk_sumcase TL TR T l r = Const (@{const_name "sum.sum_case"}, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
+fun mk_sumcase TL TR T l r = Const (@{const_name sum.sum_case}, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
 
 val App = curry op $
 
 fun mk_inj ST n i = 
     access_top_down 
     { init = (ST, I : term -> term),
-      left = (fn (T as Type ("+", [LT, RT]), inj) => (LT, inj o App (Const (@{const_name "Inl"}, LT --> T)))),
-      right =(fn (T as Type ("+", [LT, RT]), inj) => (RT, inj o App (Const (@{const_name "Inr"}, RT --> T))))} n i 
+      left = (fn (T as Type ("+", [LT, RT]), inj) => (LT, inj o App (Const (@{const_name Inl}, LT --> T)))),
+      right =(fn (T as Type ("+", [LT, RT]), inj) => (RT, inj o App (Const (@{const_name Inr}, RT --> T))))} n i 
     |> snd
 
 fun mk_proj ST n i = 
     access_top_down 
     { init = (ST, I : term -> term),
-      left = (fn (T as Type ("+", [LT, RT]), proj) => (LT, App (Const (@{const_name "Datatype.Projl"}, T --> LT)) o proj)),
-      right =(fn (T as Type ("+", [LT, RT]), proj) => (RT, App (Const (@{const_name "Datatype.Projr"}, T --> RT)) o proj))} n i
+      left = (fn (T as Type ("+", [LT, RT]), proj) => (LT, App (Const (@{const_name Datatype.Projl}, T --> LT)) o proj)),
+      right =(fn (T as Type ("+", [LT, RT]), proj) => (RT, App (Const (@{const_name Datatype.Projr}, T --> RT)) o proj))} n i
     |> snd
 
 fun mk_sumcases T fs =
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Fri Sep 18 14:40:24 2009 +0200
@@ -79,14 +79,14 @@
 
 
 (* concrete versions for sum types *)
-fun is_inj (Const ("Sum_Type.Inl", _) $ _) = true
-  | is_inj (Const ("Sum_Type.Inr", _) $ _) = true
+fun is_inj (Const (@{const_name Sum_Type.Inl}, _) $ _) = true
+  | is_inj (Const (@{const_name Sum_Type.Inr}, _) $ _) = true
   | is_inj _ = false
 
-fun dest_inl (Const ("Sum_Type.Inl", _) $ t) = SOME t
+fun dest_inl (Const (@{const_name Sum_Type.Inl}, _) $ t) = SOME t
   | dest_inl _ = NONE
 
-fun dest_inr (Const ("Sum_Type.Inr", _) $ t) = SOME t
+fun dest_inr (Const (@{const_name Sum_Type.Inr}, _) $ t) = SOME t
   | dest_inr _ = NONE
 
 
@@ -145,8 +145,8 @@
 
 fun mk_sum_skel rel =
   let
-    val cs = FundefLib.dest_binop_list @{const_name union} rel
-    fun collect_pats (Const ("Collect", _) $ Abs (_, _, c)) =
+    val cs = FundefLib.dest_binop_list @{const_name Set.union} rel
+    fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
       let
         val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
           = Term.strip_qnt_body "Ex" c
@@ -179,7 +179,7 @@
 fun get_descent (_, _, _, _, D) c m1 m2 =
   Term3tab.lookup D (c, (m1, m2))
 
-fun dest_call D (Const ("Collect", _) $ Abs (_, _, c)) =
+fun dest_call D (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
   let
     val n = get_num_points D
     val (sk, _, _, _, _) = D
@@ -233,13 +233,13 @@
 fun CALLS tac i st =
   if Thm.no_prems st then all_tac st
   else case Thm.term_of (Thm.cprem_of st i) of
-    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name union} rel, i) st
+    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Set.union} rel, i) st
   |_ => no_tac st
 
 type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
 
 fun TERMINATION ctxt tac =
-  SUBGOAL (fn (_ $ (Const (@{const_name "wf"}, wfT) $ rel), i) =>
+  SUBGOAL (fn (_ $ (Const (@{const_name wf}, wfT) $ rel), i) =>
   let
     val (T, _) = HOLogic.dest_prodT (HOLogic.dest_setT (domain_type wfT))
   in
@@ -293,7 +293,7 @@
           if null ineqs then
               Const (@{const_name Set.empty}, fastype_of rel)
           else
-              foldr1 (HOLogic.mk_binop @{const_name union}) (map mk_compr ineqs)
+              foldr1 (HOLogic.mk_binop @{const_name Set.union}) (map mk_compr ineqs)
 
       fun solve_membership_tac i =
           (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Sep 18 14:40:24 2009 +0200
@@ -81,7 +81,7 @@
    else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
 | Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_) =>
    if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox
-| Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_)) =>
+| Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_)) =>
    if term_of x aconv y then
    NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox
 | _ => Nox)
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML	Fri Sep 18 14:40:24 2009 +0200
@@ -52,18 +52,18 @@
 
 local
  fun isnum t = case t of 
-   Const(@{const_name "HOL.zero"},_) => true
- | Const(@{const_name "HOL.one"},_) => true
+   Const(@{const_name HOL.zero},_) => true
+ | Const(@{const_name HOL.one},_) => true
  | @{term "Suc"}$s => isnum s
  | @{term "nat"}$s => isnum s
  | @{term "int"}$s => isnum s
- | Const(@{const_name "HOL.uminus"},_)$s => isnum s
- | Const(@{const_name "HOL.plus"},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name "HOL.times"},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name "HOL.minus"},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name "Power.power"},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name "Divides.mod"},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name "Divides.div"},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name HOL.uminus},_)$s => isnum s
+ | Const(@{const_name HOL.plus},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name HOL.times},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name HOL.minus},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
  | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t
 
  fun ty cts t = 
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Tools/Qelim/qelim.ML
--- a/src/HOL/Tools/Qelim/qelim.ML	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Fri Sep 18 14:40:24 2009 +0200
@@ -29,8 +29,8 @@
             @{const_name "op -->"}, @{const_name "op ="}] s
        then binop_conv (conv env) p 
        else atcv env p
-  | Const(@{const_name "Not"},_)$_ => arg_conv (conv env) p
-  | Const(@{const_name "Ex"},_)$Abs(s,_,_) =>
+  | Const(@{const_name Not},_)$_ => arg_conv (conv env) p
+  | Const(@{const_name Ex},_)$Abs(s,_,_) =>
     let
      val (e,p0) = Thm.dest_comb p
      val (x,p') = Thm.dest_abs (SOME s) p0
@@ -41,8 +41,8 @@
      val (l,r) = Thm.dest_equals (cprop_of th')
     in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
        else Thm.transitive (Thm.transitive th th') (conv env r) end
-  | Const(@{const_name "Ex"},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
-  | Const(@{const_name "All"},_)$_ =>
+  | Const(@{const_name Ex},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
+  | Const(@{const_name All},_)$_ =>
     let
      val p = Thm.dest_arg p
      val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/TFL/rules.ML	Fri Sep 18 14:40:24 2009 +0200
@@ -456,7 +456,7 @@
 fun is_cong thm =
   case (Thm.prop_of thm)
      of (Const("==>",_)$(Const("Trueprop",_)$ _) $
-         (Const("==",_) $ (Const (@{const_name "Recdef.cut"},_) $ f $ R $ a $ x) $ _)) => false
+         (Const("==",_) $ (Const (@{const_name Recdef.cut},_) $ f $ R $ a $ x) $ _)) => false
       | _ => true;
 
 
@@ -659,7 +659,7 @@
   end;
 
 fun restricted t = isSome (S.find_term
-                            (fn (Const(@{const_name "Recdef.cut"},_)) =>true | _ => false)
+                            (fn (Const(@{const_name Recdef.cut},_)) =>true | _ => false)
                             t)
 
 fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Tools/TFL/usyntax.ML
--- a/src/HOL/Tools/TFL/usyntax.ML	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML	Fri Sep 18 14:40:24 2009 +0200
@@ -398,7 +398,7 @@
         end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure"
    else raise USYN_ERR "dest_relation" "not a boolean term";
 
-fun is_WFR (Const(@{const_name "Wellfounded.wf"},_)$_) = true
+fun is_WFR (Const(@{const_name Wellfounded.wf},_)$_) = true
   | is_WFR _                 = false;
 
 fun ARB ty = mk_select{Bvar=Free("v",ty),
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Tools/float_syntax.ML
--- a/src/HOL/Tools/float_syntax.ML	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/float_syntax.ML	Fri Sep 18 14:40:24 2009 +0200
@@ -27,10 +27,10 @@
 fun mk_frac str =
   let
     val {mant=i, exp = n} = Syntax.read_float str;
-    val exp = Syntax.const @{const_name "Power.power"};
+    val exp = Syntax.const @{const_name Power.power};
     val ten = mk_number 10;
     val exp10 = if n=1 then ten else exp $ ten $ (mk_number n);
-  in (Syntax.const @{const_name "divide"}) $ (mk_number i) $ exp10 end
+  in (Syntax.const @{const_name divide}) $ (mk_number i) $ exp10 end
 in
 
 fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/inductive.ML	Fri Sep 18 14:40:24 2009 +0200
@@ -86,13 +86,13 @@
 (** theory context references **)
 
 val inductive_forall_name = "HOL.induct_forall";
-val inductive_forall_def = thm "induct_forall_def";
+val inductive_forall_def = @{thm induct_forall_def};
 val inductive_conj_name = "HOL.induct_conj";
-val inductive_conj_def = thm "induct_conj_def";
-val inductive_conj = thms "induct_conj";
-val inductive_atomize = thms "induct_atomize";
-val inductive_rulify = thms "induct_rulify";
-val inductive_rulify_fallback = thms "induct_rulify_fallback";
+val inductive_conj_def = @{thm induct_conj_def};
+val inductive_conj = @{thms induct_conj};
+val inductive_atomize = @{thms induct_atomize};
+val inductive_rulify = @{thms induct_rulify};
+val inductive_rulify_fallback = @{thms induct_rulify_fallback};
 
 val notTrueE = TrueI RSN (2, notE);
 val notFalseI = Seq.hd (atac 1 notI);
@@ -176,7 +176,7 @@
     case concl of
       Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
     | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
-    | _ $ (Const ("HOL.ord_class.less_eq", _) $ _ $ _) =>
+    | _ $ (Const (@{const_name HOL.less_eq}, _) $ _ $ _) =>
       [dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
          (resolve_tac [le_funI, le_boolI'])) thm))]
     | _ => [thm]
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Fri Sep 18 14:40:24 2009 +0200
@@ -74,8 +74,8 @@
         in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
           (p (fold (Logic.all o Var) vs t) f)
         end;
-      fun mkop "op &" T x = SOME (Const (@{const_name inter}, T --> T --> T), x)
-        | mkop "op |" T x = SOME (Const (@{const_name union}, T --> T --> T), x)
+      fun mkop "op &" T x = SOME (Const (@{const_name Set.inter}, T --> T --> T), x)
+        | mkop "op |" T x = SOME (Const (@{const_name Set.union}, T --> T --> T), x)
         | mkop _ _ _ = NONE;
       fun mk_collect p T t =
         let val U = HOLogic.dest_setT T
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Tools/int_arith.ML
--- a/src/HOL/Tools/int_arith.ML	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/int_arith.ML	Fri Sep 18 14:40:24 2009 +0200
@@ -49,13 +49,13 @@
   make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
   proc = proc1, identifier = []};
 
-fun check (Const (@{const_name "HOL.one"}, @{typ int})) = false
-  | check (Const (@{const_name "HOL.one"}, _)) = true
+fun check (Const (@{const_name HOL.one}, @{typ int})) = false
+  | check (Const (@{const_name HOL.one}, _)) = true
   | check (Const (s, _)) = member (op =) [@{const_name "op ="},
-      @{const_name "HOL.times"}, @{const_name "HOL.uminus"},
-      @{const_name "HOL.minus"}, @{const_name "HOL.plus"},
-      @{const_name "HOL.zero"},
-      @{const_name "HOL.less"}, @{const_name "HOL.less_eq"}] s
+      @{const_name HOL.times}, @{const_name HOL.uminus},
+      @{const_name HOL.minus}, @{const_name HOL.plus},
+      @{const_name HOL.zero},
+      @{const_name HOL.less}, @{const_name HOL.less_eq}] s
   | check (a $ b) = check a andalso check b
   | check _ = false;
 
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Fri Sep 18 14:40:24 2009 +0200
@@ -51,7 +51,7 @@
     atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
   | _ => [thm];
 
-fun neg_prop ((TP as Const("Trueprop", _)) $ (Const (@{const_name "Not"}, _) $ t)) = TP $ t
+fun neg_prop ((TP as Const("Trueprop", _)) $ (Const (@{const_name Not}, _) $ t)) = TP $ t
   | neg_prop ((TP as Const("Trueprop", _)) $ t) = TP $ (HOLogic.Not $t)
   | neg_prop t = raise TERM ("neg_prop", [t]);
 
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/Transitive_Closure.thy	Fri Sep 18 14:40:24 2009 +0200
@@ -77,7 +77,7 @@
 subsection {* Reflexive-transitive closure *}
 
 lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r Un Id)"
-  by (simp add: expand_fun_eq)
+  by (simp add: expand_fun_eq sup2_iff)
 
 lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*"
   -- {* @{text rtrancl} of @{text r} contains @{text r} *}
diff -r e7fe01b74a92 -r c0056c2c1d17 src/HOL/UNITY/ProgressSets.thy
--- a/src/HOL/UNITY/ProgressSets.thy	Fri Sep 18 14:40:06 2009 +0200
+++ b/src/HOL/UNITY/ProgressSets.thy	Fri Sep 18 14:40:24 2009 +0200
@@ -534,7 +534,7 @@
 subsubsection{*Commutativity of Functions and Relation*}
 text{*Thesis, page 109*}
 
-(*FIXME: this proof is an ungodly mess*)
+(*FIXME: this proof is still an ungodly mess*)
 text{*From Meier's thesis, section 4.5.6*}
 lemma commutativity2_lemma:
   assumes dcommutes: 
@@ -548,36 +548,35 @@
       and TL: "T \<in> L"
       and Fstable: "F \<in> stable T"
   shows  "commutes F T B L"
-apply (simp add: commutes_def del: Int_subset_iff, clarify)  
-apply (rename_tac t)
-apply (subgoal_tac "\<exists>s. (s,t) \<in> relcl L & s \<in> T \<inter> wp act M") 
- prefer 2 
- apply (force simp add: cl_eq_Collect_relcl [OF lattice], simp, clarify) 
-apply (subgoal_tac "\<forall>u\<in>L. s \<in> u --> t \<in> u") 
- prefer 2 
- apply (intro ballI impI) 
- apply (subst cl_ident [symmetric], assumption)
- apply (simp add: relcl_def)  
- apply (blast intro: cl_mono [THEN [2] rev_subsetD])  
-apply (subgoal_tac "funof act s \<in> T\<inter>M") 
- prefer 2 
- apply (cut_tac Fstable) 
- apply (force intro!: funof_in 
-              simp add: wp_def stable_def constrains_def determ total) 
-apply (subgoal_tac "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L")
- prefer 2
- apply (rule dcommutes [rule_format], assumption+) 
-apply (subgoal_tac "t \<in> B | funof act t \<in> cl L (T\<inter>M)")
- prefer 2 
- apply (simp add: relcl_def)
- apply (blast intro: BL cl_mono [THEN [2] rev_subsetD])  
-apply (subgoal_tac "t \<in> B | t \<in> wp act (cl L (T\<inter>M))")
- prefer 2
- apply (blast intro: funof_imp_wp determ) 
-apply (blast intro: TL cl_mono [THEN [2] rev_subsetD])  
-done
-
-
+apply (simp add: commutes_def del: Int_subset_iff le_inf_iff, clarify)
+proof -
+  fix M and act and t
+  assume 1: "B \<subseteq> M" "act \<in> Acts F" "t \<in> cl L (T \<inter> wp act M)"
+  then have "\<exists>s. (s,t) \<in> relcl L \<and> s \<in> T \<inter> wp act M"
+    by (force simp add: cl_eq_Collect_relcl [OF lattice])
+  then obtain s where 2: "(s, t) \<in> relcl L" "s \<in> T" "s \<in> wp act M"
+    by blast
+  then have 3: "\<forall>u\<in>L. s \<in> u --> t \<in> u"
+    apply (intro ballI impI) 
+    apply (subst cl_ident [symmetric], assumption)
+    apply (simp add: relcl_def)  
+    apply (blast intro: cl_mono [THEN [2] rev_subsetD])
+    done
+  with 1 2 Fstable have 4: "funof act s \<in> T\<inter>M"
+    by (force intro!: funof_in 
+      simp add: wp_def stable_def constrains_def determ total)
+  with 1 2 3 have 5: "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
+    by (intro dcommutes [rule_format]) assumption+ 
+  with 1 2 3 4 have "t \<in> B | funof act t \<in> cl L (T\<inter>M)"
+    by (simp add: relcl_def) (blast intro: BL cl_mono [THEN [2] rev_subsetD])  
+  with 1 2 3 4 5 have "t \<in> B | t \<in> wp act (cl L (T\<inter>M))"
+    by (blast intro: funof_imp_wp determ) 
+  with 2 3 have "t \<in> T \<and> (t \<in> B \<or> t \<in> wp act (cl L (T \<inter> M)))"
+    by (blast intro: TL cl_mono [THEN [2] rev_subsetD])
+  then show "t \<in> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))"
+    by simp
+qed
+  
 text{*Version packaged with @{thm progress_set_Union}*}
 lemma commutativity2:
   assumes leadsTo: "F \<in> A leadsTo B"