src/HOL/ex/RPred.thy
changeset 44845 5e51075cbd97
parent 42463 f270e3e18be5
     1.1 --- a/src/HOL/ex/RPred.thy	Thu Sep 08 08:41:28 2011 -0700
     1.2 +++ b/src/HOL/ex/RPred.thy	Fri Sep 09 00:22:18 2011 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4  (* (infixl "\<squnion>" 80) *)
     1.5  where
     1.6    "supp RP1 RP2 = (\<lambda>s. let (P1, s') = RP1 s; (P2, s'') = RP2 s'
     1.7 -  in (semilattice_sup_class.sup P1 P2, s''))"
     1.8 +  in (sup_class.sup P1 P2, s''))"
     1.9  
    1.10  definition if_rpred :: "bool \<Rightarrow> unit rpred"
    1.11  where