Ramana and Robert, matrix multiplication in HOL Light is defined in the Multivariate directory. I'm not a real expert on this, but you can find examples of Multivariate-powered matrix multiplication in http://code.google.com/p/hol-light/source/browse/trunk/RichterHilbertAxiomGeometry/inverse_bug_puzzle_read.ml?spec=svn179&r=179 which begins with needs "Multivariate/determinants.ml";;
-- Best, Bill ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
