# HG changeset patch
# User nipkow
# Date 1288365922 -7200
# Node ID 6014e8252e5748ad95c0619745530738332a6311
# Parent  151fef6523243d1fab78d0e8c00479f6fc25ebc5
hide Sum_Type.Plus

diff -r 151fef652324 -r 6014e8252e57 src/HOL/Algebra/AbelCoset.thy
--- a/src/HOL/Algebra/AbelCoset.thy	Fri Oct 29 16:04:35 2010 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy	Fri Oct 29 17:25:22 2010 +0200
@@ -13,7 +13,7 @@
 text {* Hiding @{text "<+>"} from @{theory Sum_Type} until I come
   up with better syntax here *}
 
-no_notation Plus (infixr "<+>" 65)
+no_notation Sum_Type.Plus (infixr "<+>" 65)
 
 definition
   a_r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "+>\<index>" 60)
diff -r 151fef652324 -r 6014e8252e57 src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Fri Oct 29 16:04:35 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Fri Oct 29 17:25:22 2010 +0200
@@ -105,7 +105,7 @@
 
 section {* Example symbolic derivation *}
 
-hide_const Plus Pow
+hide_const Pow
 
 datatype expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr
   | Minus expr expr | Uminus expr | Pow expr int | Exp expr
diff -r 151fef652324 -r 6014e8252e57 src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Fri Oct 29 16:04:35 2010 +0200
+++ b/src/HOL/Sum_Type.thy	Fri Oct 29 17:25:22 2010 +0200
@@ -162,6 +162,8 @@
 definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set" (infixr "<+>" 65) where
   "A <+> B = Inl ` A \<union> Inr ` B"
 
+hide_const (open) Plus --"Valuable identifier"
+
 lemma InlI [intro!]: "a \<in> A \<Longrightarrow> Inl a \<in> A <+> B"
 by (simp add: Plus_def)