# HG changeset patch
# User krauss
# Date 1288343081 -7200
# Node ID 029400b6c8939df698f0333eb1b9c4fb9884e797
# Parent  63405dd65b0d5dc8078d6817ee87affb1fa7a45a
hide_const various constants, in particular to avoid ugly qualifiers in HOLCF

diff -r 63405dd65b0d -r 029400b6c893 src/HOL/Complete_Partial_Order.thy
--- 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
diff -r 63405dd65b0d -r 029400b6c893 src/HOL/Partial_Function.thy
--- 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