Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
sum_case is now authentic.
authorberghofe
Tue, 24 Apr 2007 15:17:22 +0200
changeset 22781 18fbba942a80
parent 22780 41162a270151
child 22782 8bc6fbbe1d0f
sum_case is now authentic.
src/HOL/Bali/Basis.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Bali/Basis.thy	Tue Apr 24 15:15:52 2007 +0200
+++ b/src/HOL/Bali/Basis.thy	Tue Apr 24 15:17:22 2007 +0200
@@ -216,7 +216,7 @@
 syntax
   fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
 translations
- "fun_sum" == "sum_case"
+ "fun_sum" == "CONST sum_case"
 
 consts    the_Inl  :: "'a + 'b \<Rightarrow> 'a"
           the_Inr  :: "'a + 'b \<Rightarrow> 'b"
isabelle