hide Sum_Type.Plus
authornipkow
Fri Oct 29 17:25:22 2010 +0200 (2010-10-29)
changeset 402716014e8252e57
parent 40269 151fef652324
child 40272 b12ae2445985
hide Sum_Type.Plus
src/HOL/Algebra/AbelCoset.thy
src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
src/HOL/Sum_Type.thy
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Fri Oct 29 16:04:35 2010 +0200
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Fri Oct 29 17:25:22 2010 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  text {* Hiding @{text "<+>"} from @{theory Sum_Type} until I come
     1.5    up with better syntax here *}
     1.6  
     1.7 -no_notation Plus (infixr "<+>" 65)
     1.8 +no_notation Sum_Type.Plus (infixr "<+>" 65)
     1.9  
    1.10  definition
    1.11    a_r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "+>\<index>" 60)
     2.1 --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Fri Oct 29 16:04:35 2010 +0200
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Fri Oct 29 17:25:22 2010 +0200
     2.3 @@ -105,7 +105,7 @@
     2.4  
     2.5  section {* Example symbolic derivation *}
     2.6  
     2.7 -hide_const Plus Pow
     2.8 +hide_const Pow
     2.9  
    2.10  datatype expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr
    2.11    | Minus expr expr | Uminus expr | Pow expr int | Exp expr
     3.1 --- a/src/HOL/Sum_Type.thy	Fri Oct 29 16:04:35 2010 +0200
     3.2 +++ b/src/HOL/Sum_Type.thy	Fri Oct 29 17:25:22 2010 +0200
     3.3 @@ -162,6 +162,8 @@
     3.4  definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set" (infixr "<+>" 65) where
     3.5    "A <+> B = Inl ` A \<union> Inr ` B"
     3.6  
     3.7 +hide_const (open) Plus --"Valuable identifier"
     3.8 +
     3.9  lemma InlI [intro!]: "a \<in> A \<Longrightarrow> Inl a \<in> A <+> B"
    3.10  by (simp add: Plus_def)
    3.11