src/HOL/Induct/BinaryTree_Map.thy
Wed, 10 Dec 2003 15:59:34 +0100 paulson Moving some theorems from Real/RealArith0.ML
less more (0) tip