(*-------------------------------------------------------------------------*)
(*
   File:         unity
   Description:

   This file loads and opens the HOL Light theory unity, called HOL_UNITY

   Author:       Flemming Andersen
   Date:         November 17, 2003
*)
(*-------------------------------------------------------------------------*)

loadt "Examples/hol88.ml";;

loadt "Unity/aux_definitions.ml";;
loadt "Unity/mk_state_logic.ml";;
loadt "Unity/mk_unless.ml";;
loadt "Unity/mk_ensures.ml";;
loadt "Unity/mk_gen_induct.ml";;
loadt "Unity/mk_leadsto.ml";;
loadt "Unity/mk_comp_unity.ml";;
loadt "Unity/mk_unity_prog.ml";;