# HG changeset patch
# User wenzelm
# Date 1082629103 -7200
# Node ID aad262a360146ef6393bd928e99085a6df6bb8b2
# Parent  0848ab6fe5fc46008cb2bb6b379082b27858a95b
fixed constdefs typing;

diff -r 0848ab6fe5fc -r aad262a36014 src/HOL/Matrix/MatrixGeneral.thy
--- a/src/HOL/Matrix/MatrixGeneral.thy	Thu Apr 22 12:11:17 2004 +0200
+++ b/src/HOL/Matrix/MatrixGeneral.thy	Thu Apr 22 12:18:23 2004 +0200
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Matrix/MatrixGeneral.thy
     ID:         $Id$
     Author:     Steven Obua
-    License:    2004 Technische Universität München
+    License:    2004 Technische UniversitÃ\<currency>t MÃ\<onequarter>nchen
 *)
 
 theory MatrixGeneral = Main:
@@ -329,9 +329,9 @@
   by (simp add: ncols_le)
 
 constdefs
-  zero_r_neutral :: "('a \<Rightarrow> ('b::zero) \<Rightarrow> 'a) \<Rightarrow> bool"
+  zero_r_neutral :: "('a \<Rightarrow> 'b::zero \<Rightarrow> 'a) \<Rightarrow> bool"
   "zero_r_neutral f == ! a. f a 0 = a"
-  zero_l_neutral :: "('a \<Rightarrow> ('b::zero) \<Rightarrow> 'a) \<Rightarrow> bool"
+  zero_l_neutral :: "('a::zero \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"
   "zero_l_neutral f == ! a. f 0 a = a"
   zero_closed :: "(('a::zero) \<Rightarrow> ('b::zero) \<Rightarrow> ('c::zero)) \<Rightarrow> bool"
   "zero_closed f == (!x. f x 0 = 0) & (!y. f 0 y = 0)"