Hi, I just discovered that another last minute "FIXME" has changed the hierarchy of rings in Isabelle2007 such that "real" is not of sort "lordered_ring" any more. More generally, "ordered_ring" is not an "lordered_ring" any more. This is pretty unfortunate as it renders the whole HOL-Complex-Matrix package in Isabelle 2007 garbage. Maybe in the future one should refrain from last minute fixes which one does not fully understand.
Steven
