Unity/make.ml

   1 (*-------------------------------------------------------------------------*)
   2 (*
   3    File:         unity
   4    Description:
   5
   6    This file loads and opens the HOL Light theory unity, called HOL_UNITY
   7
   8    Author:       Flemming Andersen
   9    Date:         November 17, 2003
  10 *)
  11 (*-------------------------------------------------------------------------*)
  12
  13 loadt "Examples/hol88.ml";;
  14
  15 loadt "Unity/aux_definitions.ml";;
  16 loadt "Unity/mk_state_logic.ml";;
  17 loadt "Unity/mk_unless.ml";;
  18 loadt "Unity/mk_ensures.ml";;
  19 loadt "Unity/mk_gen_induct.ml";;
  20 loadt "Unity/mk_leadsto.ml";;
  21 loadt "Unity/mk_comp_unity.ml";;
  22 loadt "Unity/mk_unity_prog.ml";;