(**************************************************************************)
(*                                                                        *)
(* 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                   *)
(*                                                                        *)
(**************************************************************************)