Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/RPred.thy
changeset 35028 108662d50512
parent 33142 edab304696ec
child 36176 3fe7e97ccca8 
--- a/src/HOL/ex/RPred.thy	Fri Feb 05 14:33:31 2010 +0100
+++ b/src/HOL/ex/RPred.thy	Fri Feb 05 14:33:50 2010 +0100
@@ -25,7 +25,7 @@
 (* (infixl "\<squnion>" 80) *)
 where
   "supp RP1 RP2 = (\<lambda>s. let (P1, s') = RP1 s; (P2, s'') = RP2 s'
-  in (upper_semilattice_class.sup P1 P2, s''))"
+  in (semilattice_sup_class.sup P1 P2, s''))"
 
 definition if_rpred :: "bool \<Rightarrow> unit rpred"
 where
isabelle