src/HOL/Real.thy
author wenzelm
Tue, 16 Dec 2008 19:24:55 +0100
changeset 29127 2a684ee023e7
parent 29108 12ca66b887a0
child 29197 6d4cb27ed19c
permissions -rw-r--r--
proper document antiquotations;

theory Real
imports RComplete "~~/src/HOL/Real/RealVector"
begin

end