src/HOL/Matrix/MatrixGeneral.thy

 (*  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:
 
 types 'a infmatrix = "[nat, nat] \<Rightarrow> 'a"

 
 lemma combine_ncols: "f 0 0 = 0 \<Longrightarrow> ncols A <= q \<Longrightarrow> ncols B <= q \<Longrightarrow> ncols(combine_matrix f A B) <= q"
   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)"
 
 consts foldseq :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"