--- 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)
--- 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
--- 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)