--- /dev/null
+(**************************************************************************)
+(* *)
+(* Landau's "Grundlagen der Analysis", formal specification for AUTOMATH *)
+(* Copyright (C) 1977, L.S. van Benthem Jutting *)
+(* 1992, revised by F. Wiedijk *)
+(* 2008, 2014, revised by F. Guidi *)
+(* *)
+(* Mechanized translation for COQ version 8 by F. Guidi *)
+(* *)
+(**************************************************************************)
+