1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
(*-------------------------------------------------------------------------*)
(*
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";;
|
