src/HOL/Real.thy
author huffman
Sat Jun 06 09:11:12 2009 -0700 (2009-06-06)
changeset 31488 5691ccb8d6b5
parent 29197 6d4cb27ed19c
child 32877 6f09346c7c08
permissions -rw-r--r--
generalize tendsto to class topological_space
haftmann@28952
     1
theory Real
haftmann@29197
     2
imports RComplete RealVector
haftmann@28952
     3
begin
wenzelm@19640
     4
wenzelm@19640
     5
end