--- a/src/HOL/Complete_Partial_Order.thy Fri Oct 29 10:40:36 2010 +0200
+++ b/src/HOL/Complete_Partial_Order.thy Fri Oct 29 11:04:41 2010 +0200
@@ -258,6 +258,6 @@
end
-
+hide_const (open) lub iterates fixp admissible
end
--- a/src/HOL/Partial_Function.thy Fri Oct 29 10:40:36 2010 +0200
+++ b/src/HOL/Partial_Function.thy Fri Oct 29 11:04:41 2010 +0200
@@ -242,6 +242,7 @@
show "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y'. C y' g))" .
qed
+hide_const (open) chain
end