added syntactic classes for "inf" and "sup"
authorkrauss
Fri Sep 09 00:22:18 2011 +0200 (2011-09-09)
changeset 448455e51075cbd97
parent 44844 f74a4175a3a8
child 44847 b93d17a52217
added syntactic classes for "inf" and "sup"
NEWS
src/HOL/Big_Operators.thy
src/HOL/Complete_Lattice.thy
src/HOL/GCD.thy
src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
src/HOL/Import/HOLLight/hollight.imp
src/HOL/Lattices.thy
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Quickcheck.thy
src/HOL/ex/Quickcheck_Lattice_Examples.thy
src/HOL/ex/RPred.thy
     1.1 --- a/NEWS	Thu Sep 08 08:41:28 2011 -0700
     1.2 +++ b/NEWS	Fri Sep 09 00:22:18 2011 +0200
     1.3 @@ -131,6 +131,10 @@
     1.4  
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Added syntactic classes "inf" and "sup" for the respective
     1.8 +constants.  INCOMPATIBILITY: Changes in the argument order of the
     1.9 +(mostly internal) locale predicates for some derived classes.
    1.10 +
    1.11  * Theorem collections ball_simps and bex_simps do not contain theorems
    1.12  referring to UNION any longer; these have been moved to collection
    1.13  UN_ball_bex_simps.  INCOMPATIBILITY.
     2.1 --- a/src/HOL/Big_Operators.thy	Thu Sep 08 08:41:28 2011 -0700
     2.2 +++ b/src/HOL/Big_Operators.thy	Fri Sep 09 00:22:18 2011 +0200
     2.3 @@ -1517,7 +1517,7 @@
     2.4    proof qed (auto simp add: max_def)
     2.5  
     2.6  lemma max_lattice:
     2.7 -  "class.semilattice_inf (op \<ge>) (op >) max"
     2.8 +  "class.semilattice_inf max (op \<ge>) (op >)"
     2.9    by (fact min_max.dual_semilattice)
    2.10  
    2.11  lemma dual_max:
    2.12 @@ -1611,7 +1611,7 @@
    2.13    assumes "finite A" and "x \<in> A"
    2.14    shows "x \<le> Max A"
    2.15  proof -
    2.16 -  interpret semilattice_inf "op \<ge>" "op >" max
    2.17 +  interpret semilattice_inf max "op \<ge>" "op >"
    2.18      by (rule max_lattice)
    2.19    from assms show ?thesis by (simp add: Max_def fold1_belowI)
    2.20  qed
    2.21 @@ -1625,7 +1625,7 @@
    2.22    assumes "finite A" and "A \<noteq> {}"
    2.23    shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
    2.24  proof -
    2.25 -  interpret semilattice_inf "op \<ge>" "op >" max
    2.26 +  interpret semilattice_inf max "op \<ge>" "op >"
    2.27      by (rule max_lattice)
    2.28    from assms show ?thesis by (simp add: Max_def below_fold1_iff)
    2.29  qed
     3.1 --- a/src/HOL/Complete_Lattice.thy	Thu Sep 08 08:41:28 2011 -0700
     3.2 +++ b/src/HOL/Complete_Lattice.thy	Fri Sep 09 00:22:18 2011 +0200
     3.3 @@ -33,7 +33,7 @@
     3.4  begin
     3.5  
     3.6  lemma dual_complete_lattice:
     3.7 -  "class.complete_lattice Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom>"
     3.8 +  "class.complete_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
     3.9    by (auto intro!: class.complete_lattice.intro dual_bounded_lattice)
    3.10      (unfold_locales, (fact bot_least top_greatest
    3.11          Sup_upper Sup_least Inf_lower Inf_greatest)+)
    3.12 @@ -85,7 +85,7 @@
    3.13  lemma INF_foundation_dual [no_atp]:
    3.14    "complete_lattice.SUPR Inf = INFI"
    3.15  proof (rule ext)+
    3.16 -  interpret dual: complete_lattice Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
    3.17 +  interpret dual: complete_lattice Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
    3.18      by (fact dual_complete_lattice)
    3.19    fix f :: "'b \<Rightarrow> 'a" and A
    3.20    show "complete_lattice.SUPR Inf A f = (\<Sqinter>a\<in>A. f a)"
    3.21 @@ -95,7 +95,7 @@
    3.22  lemma SUP_foundation_dual [no_atp]:
    3.23    "complete_lattice.INFI Sup = SUPR"
    3.24  proof (rule ext)+
    3.25 -  interpret dual: complete_lattice Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
    3.26 +  interpret dual: complete_lattice Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
    3.27      by (fact dual_complete_lattice)
    3.28    fix f :: "'b \<Rightarrow> 'a" and A
    3.29    show "complete_lattice.INFI Sup A f = (\<Squnion>a\<in>A. f a)"
    3.30 @@ -313,7 +313,7 @@
    3.31    "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
    3.32    "\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?Q)
    3.33  proof -
    3.34 -  interpret dual: complete_lattice Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
    3.35 +  interpret dual: complete_lattice Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
    3.36      by (fact dual_complete_lattice)
    3.37    from dual.Inf_top_conv show ?P and ?Q by simp_all
    3.38  qed
    3.39 @@ -407,7 +407,7 @@
    3.40    by (simp add: SUP_def inf_Sup image_image)
    3.41  
    3.42  lemma dual_complete_distrib_lattice:
    3.43 -  "class.complete_distrib_lattice Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom>"
    3.44 +  "class.complete_distrib_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
    3.45    apply (rule class.complete_distrib_lattice.intro)
    3.46    apply (fact dual_complete_lattice)
    3.47    apply (rule class.complete_distrib_lattice_axioms.intro)
    3.48 @@ -458,7 +458,7 @@
    3.49  begin
    3.50  
    3.51  lemma dual_complete_boolean_algebra:
    3.52 -  "class.complete_boolean_algebra Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - y) uminus"
    3.53 +  "class.complete_boolean_algebra Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - y) uminus"
    3.54    by (rule class.complete_boolean_algebra.intro, rule dual_complete_distrib_lattice, rule dual_boolean_algebra)
    3.55  
    3.56  lemma uminus_Inf:
    3.57 @@ -489,7 +489,7 @@
    3.58  begin
    3.59  
    3.60  lemma dual_complete_linorder:
    3.61 -  "class.complete_linorder Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom>"
    3.62 +  "class.complete_linorder Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
    3.63    by (rule class.complete_linorder.intro, rule dual_complete_lattice, rule dual_linorder)
    3.64  
    3.65  lemma Inf_less_iff (*[simp]*):
    3.66 @@ -537,7 +537,7 @@
    3.67  lemma Inf_eq_bot_iff (*[simp]*):
    3.68    "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
    3.69  proof -
    3.70 -  interpret dual: complete_linorder Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
    3.71 +  interpret dual: complete_linorder Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
    3.72      by (fact dual_complete_linorder)
    3.73    from dual.Sup_eq_top_iff show ?thesis .
    3.74  qed
     4.1 --- a/src/HOL/GCD.thy	Thu Sep 08 08:41:28 2011 -0700
     4.2 +++ b/src/HOL/GCD.thy	Fri Sep 09 00:22:18 2011 +0200
     4.3 @@ -1463,17 +1463,17 @@
     4.4  subsubsection {* The complete divisibility lattice *}
     4.5  
     4.6  
     4.7 -interpretation gcd_semilattice_nat: semilattice_inf "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd
     4.8 +interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
     4.9  proof
    4.10    case goal3 thus ?case by(metis gcd_unique_nat)
    4.11  qed auto
    4.12  
    4.13 -interpretation lcm_semilattice_nat: semilattice_sup "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm
    4.14 +interpretation lcm_semilattice_nat: semilattice_sup lcm "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
    4.15  proof
    4.16    case goal3 thus ?case by(metis lcm_unique_nat)
    4.17  qed auto
    4.18  
    4.19 -interpretation gcd_lcm_lattice_nat: lattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd lcm ..
    4.20 +interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm ..
    4.21  
    4.22  text{* Lifting gcd and lcm to finite (Gcd/Lcm) and infinite sets (GCD/LCM).
    4.23  GCD is defined via LCM to facilitate the proof that we have a complete lattice.
    4.24 @@ -1579,7 +1579,7 @@
    4.25  qed
    4.26  
    4.27  interpretation gcd_lcm_complete_lattice_nat:
    4.28 -  complete_lattice GCD LCM "op dvd" "%m n::nat. m dvd n & ~ n dvd m" gcd lcm 1 0
    4.29 +  complete_lattice GCD LCM gcd "op dvd" "%m n::nat. m dvd n & ~ n dvd m" lcm 1 0
    4.30  proof
    4.31    case goal1 show ?case by simp
    4.32  next
     5.1 --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Sep 08 08:41:28 2011 -0700
     5.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Fri Sep 09 00:22:18 2011 +0200
     5.3 @@ -145,9 +145,9 @@
     5.4    GEQ > HOL.eq
     5.5    GSPEC > Set.Collect
     5.6    SETSPEC > HOLLightCompat.SETSPEC
     5.7 -  UNION > Lattices.semilattice_sup_class.sup :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
     5.8 +  UNION > Lattices.sup_class.sup :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
     5.9    UNIONS > Complete_Lattice.Sup_class.Sup :: "(('a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
    5.10 -  INTER > Lattices.semilattice_inf_class.inf :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
    5.11 +  INTER > Lattices.inf_class.inf :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
    5.12    INTERS > Complete_Lattice.Inf_class.Inf :: "(('a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
    5.13    DIFF > Groups.minus_class.minus :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
    5.14    SUBSET > Orderings.ord_class.less_eq :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
     6.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Thu Sep 08 08:41:28 2011 -0700
     6.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Fri Sep 09 00:22:18 2011 +0200
     6.3 @@ -267,7 +267,7 @@
     6.4    "WF" > "Wellfounded.wfP"
     6.5    "UNIV" > "Orderings.top_class.top" :: "'a => bool"
     6.6    "UNIONS" > "Complete_Lattice.Sup_class.Sup" :: "(('a => bool) => bool) => 'a => bool"
     6.7 -  "UNION" > "Lattices.semilattice_sup_class.sup" :: "('a => bool) => ('a => bool) => 'a => bool"
     6.8 +  "UNION" > "Lattices.sup_class.sup" :: "('a => bool) => ('a => bool) => 'a => bool"
     6.9    "UNCURRY" > "HOLLight.hollight.UNCURRY"
    6.10    "TL" > "List.tl"
    6.11    "T" > "HOL.True"
    6.12 @@ -317,7 +317,7 @@
    6.13    "ITLIST" > "List.foldr"
    6.14    "ISO" > "HOLLight.hollight.ISO"
    6.15    "INTERS" > "Complete_Lattice.Inf_class.Inf" :: "(('a => bool) => bool) => 'a => bool"
    6.16 -  "INTER" > "Lattices.semilattice_inf_class.inf" :: "('a => bool) => ('a => bool) => 'a => bool"
    6.17 +  "INTER" > "Lattices.inf_class.inf" :: "('a => bool) => ('a => bool) => 'a => bool"
    6.18    "INSERT" > "Set.insert"
    6.19    "INR" > "Sum_Type.Inr"
    6.20    "INL" > "Sum_Type.Inl"
     7.1 --- a/src/HOL/Lattices.thy	Thu Sep 08 08:41:28 2011 -0700
     7.2 +++ b/src/HOL/Lattices.thy	Fri Sep 09 00:22:18 2011 +0200
     7.3 @@ -51,15 +51,18 @@
     7.4    bot ("\<bottom>") and
     7.5    top ("\<top>")
     7.6  
     7.7 +class inf =
     7.8 +  fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
     7.9  
    7.10 -class semilattice_inf = order +
    7.11 -  fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
    7.12 +class sup = 
    7.13 +  fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
    7.14 +
    7.15 +class semilattice_inf =  order + inf +
    7.16    assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
    7.17    and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
    7.18    and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
    7.19  
    7.20 -class semilattice_sup = order +
    7.21 -  fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
    7.22 +class semilattice_sup = order + sup +
    7.23    assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
    7.24    and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
    7.25    and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
    7.26 @@ -68,7 +71,7 @@
    7.27  text {* Dual lattice *}
    7.28  
    7.29  lemma dual_semilattice:
    7.30 -  "class.semilattice_inf greater_eq greater sup"
    7.31 +  "class.semilattice_inf sup greater_eq greater"
    7.32  by (rule class.semilattice_inf.intro, rule dual_order)
    7.33    (unfold_locales, simp_all add: sup_least)
    7.34  
    7.35 @@ -236,7 +239,7 @@
    7.36  begin
    7.37  
    7.38  lemma dual_lattice:
    7.39 -  "class.lattice (op \<ge>) (op >) sup inf"
    7.40 +  "class.lattice sup (op \<ge>) (op >) inf"
    7.41    by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
    7.42      (unfold_locales, auto)
    7.43  
    7.44 @@ -307,7 +310,7 @@
    7.45  lemma less_supI1:
    7.46    "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b"
    7.47  proof -
    7.48 -  interpret dual: semilattice_inf "op \<ge>" "op >" sup
    7.49 +  interpret dual: semilattice_inf sup "op \<ge>" "op >"
    7.50      by (fact dual_semilattice)
    7.51    assume "x \<sqsubset> a"
    7.52    then show "x \<sqsubset> a \<squnion> b"
    7.53 @@ -317,7 +320,7 @@
    7.54  lemma less_supI2:
    7.55    "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b"
    7.56  proof -
    7.57 -  interpret dual: semilattice_inf "op \<ge>" "op >" sup
    7.58 +  interpret dual: semilattice_inf sup "op \<ge>" "op >"
    7.59      by (fact dual_semilattice)
    7.60    assume "x \<sqsubset> b"
    7.61    then show "x \<sqsubset> a \<squnion> b"
    7.62 @@ -348,7 +351,7 @@
    7.63  by(simp add: inf_sup_aci inf_sup_distrib1)
    7.64  
    7.65  lemma dual_distrib_lattice:
    7.66 -  "class.distrib_lattice (op \<ge>) (op >) sup inf"
    7.67 +  "class.distrib_lattice sup (op \<ge>) (op >) inf"
    7.68    by (rule class.distrib_lattice.intro, rule dual_lattice)
    7.69      (unfold_locales, fact inf_sup_distrib1)
    7.70  
    7.71 @@ -420,7 +423,7 @@
    7.72  begin
    7.73  
    7.74  lemma dual_bounded_lattice:
    7.75 -  "class.bounded_lattice greater_eq greater sup inf \<top> \<bottom>"
    7.76 +  "class.bounded_lattice sup greater_eq greater inf \<top> \<bottom>"
    7.77    by unfold_locales (auto simp add: less_le_not_le)
    7.78  
    7.79  end
    7.80 @@ -432,7 +435,7 @@
    7.81  begin
    7.82  
    7.83  lemma dual_boolean_algebra:
    7.84 -  "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus greater_eq greater sup inf \<top> \<bottom>"
    7.85 +  "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus sup greater_eq greater inf \<top> \<bottom>"
    7.86    by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
    7.87      (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
    7.88  
    7.89 @@ -506,7 +509,7 @@
    7.90  lemma compl_sup [simp]:
    7.91    "- (x \<squnion> y) = - x \<sqinter> - y"
    7.92  proof -
    7.93 -  interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus greater_eq greater sup inf \<top> \<bottom>
    7.94 +  interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus sup greater_eq greater inf \<top> \<bottom>
    7.95      by (rule dual_boolean_algebra)
    7.96    then show ?thesis by simp
    7.97  qed
    7.98 @@ -591,7 +594,7 @@
    7.99  subsection {* @{const min}/@{const max} on linear orders as
   7.100    special case of @{const inf}/@{const sup} *}
   7.101  
   7.102 -sublocale linorder < min_max!: distrib_lattice less_eq less min max
   7.103 +sublocale linorder < min_max!: distrib_lattice min less_eq less max
   7.104  proof
   7.105    fix x y z
   7.106    show "max x (min y z) = min (max x y) (max x z)"
     8.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Sep 08 08:41:28 2011 -0700
     8.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Sep 09 00:22:18 2011 +0200
     8.3 @@ -286,8 +286,8 @@
     8.4     (@{const_name "Groups.minus_class.minus"}, @{typ "prop => prop => prop"}),
     8.5     (@{const_name "Groups.times_class.times"}, @{typ "prop => prop => prop"}),
     8.6     (@{const_name "Fields.inverse_class.divide"}, @{typ "prop => prop => prop"}),
     8.7 -   (@{const_name "Lattices.semilattice_inf_class.inf"}, @{typ "prop => prop => prop"}),
     8.8 -   (@{const_name "Lattices.semilattice_sup_class.sup"}, @{typ "prop => prop => prop"}),
     8.9 +   (@{const_name "Lattices.inf_class.inf"}, @{typ "prop => prop => prop"}),
    8.10 +   (@{const_name "Lattices.sup_class.sup"}, @{typ "prop => prop => prop"}),
    8.11     (@{const_name "Orderings.bot_class.bot"}, @{typ "prop => prop => prop"}),
    8.12     (@{const_name "Orderings.ord_class.min"}, @{typ "prop => prop => prop"}),
    8.13     (@{const_name "Orderings.ord_class.max"}, @{typ "prop => prop => prop"}),
     9.1 --- a/src/HOL/Quickcheck.thy	Thu Sep 08 08:41:28 2011 -0700
     9.2 +++ b/src/HOL/Quickcheck.thy	Fri Sep 09 00:22:18 2011 +0200
     9.3 @@ -183,7 +183,7 @@
     9.4  where
     9.5    "union R1 R2 = (\<lambda>s. let
     9.6       (P1, s') = R1 s; (P2, s'') = R2 s'
     9.7 -   in (semilattice_sup_class.sup P1 P2, s''))"
     9.8 +   in (sup_class.sup P1 P2, s''))"
     9.9  
    9.10  definition if_randompred :: "bool \<Rightarrow> unit randompred"
    9.11  where
    10.1 --- a/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Thu Sep 08 08:41:28 2011 -0700
    10.2 +++ b/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Fri Sep 09 00:22:18 2011 +0200
    10.3 @@ -125,7 +125,7 @@
    10.4    by (rule inf_absorb1) simp
    10.5  
    10.6  lemma inf_eq_top_iff [simp]:
    10.7 -  "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
    10.8 +  "(x :: 'a :: bounded_lattice_top) \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
    10.9    quickcheck[expect = no_counterexample]
   10.10    by (simp add: eq_iff)
   10.11  
    11.1 --- a/src/HOL/ex/RPred.thy	Thu Sep 08 08:41:28 2011 -0700
    11.2 +++ b/src/HOL/ex/RPred.thy	Fri Sep 09 00:22:18 2011 +0200
    11.3 @@ -25,7 +25,7 @@
    11.4  (* (infixl "\<squnion>" 80) *)
    11.5  where
    11.6    "supp RP1 RP2 = (\<lambda>s. let (P1, s') = RP1 s; (P2, s'') = RP2 s'
    11.7 -  in (semilattice_sup_class.sup P1 P2, s''))"
    11.8 +  in (sup_class.sup P1 P2, s''))"
    11.9  
   11.10  definition if_rpred :: "bool \<Rightarrow> unit rpred"
   11.11  where