sum_case is now authentic.
authorberghofe
Tue Apr 24 15:17:22 2007 +0200 (2007-04-24)
changeset 2278118fbba942a80
parent 22780 41162a270151
child 22782 8bc6fbbe1d0f
sum_case is now authentic.
src/HOL/Bali/Basis.thy
     1.1 --- a/src/HOL/Bali/Basis.thy	Tue Apr 24 15:15:52 2007 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Tue Apr 24 15:17:22 2007 +0200
     1.3 @@ -216,7 +216,7 @@
     1.4  syntax
     1.5    fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
     1.6  translations
     1.7 - "fun_sum" == "sum_case"
     1.8 + "fun_sum" == "CONST sum_case"
     1.9  
    1.10  consts    the_Inl  :: "'a + 'b \<Rightarrow> 'a"
    1.11            the_Inr  :: "'a + 'b \<Rightarrow> 'b"