Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Matrix/MatrixGeneral.thy
changeset 14654 aad262a36014
parent 14593 90c88e7ef62d
child 14662 d2c6a0f030ab 
--- 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)"
isabelle