(* ========================================================================= *)
(*       miz3: Mizar-style declarative proofs for HOL Light.                 *)
(*                                                                           *)
(*                (c) Freek Wiedijk 2009-2012                                *)
(*                                                                           *)
(*      Distributed under the same license terms as HOL Light.               *)
(*                                                                           *)
(*     See http://arxiv.org/abs/1201.3601 for more information.              *)
(* ========================================================================= *)