src/HOL/Multivariate_Analysis/Operator_Norm.thy
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
less more (0) -1 tip