1 (**************************************************************************)
3 (* Landau's "Grundlagen der Analysis", formal specification for AUTOMATH *)
4 (* Copyright (C) 1977, L.S. van Benthem Jutting *)
5 (* 1992, revised by F. Wiedijk *)
6 (* 2008, 2014, revised by F. Guidi *)
8 (* Mechanized translation for COQ version 8 by F. Guidi *)
10 (**************************************************************************)