1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
% ===================================================================== %
% FILE : load_more_arithmetic.ml %
% DESCRIPTION : creates a function that loads the contents of the %
% library "more_arithmetic" into hol. %
% %
% AUTHOR : P. Curzon %
% DATE : 8.4.91 %
% ===================================================================== %
% --------------------------------------------------------------------- %
% define the function load_more_arithmetic. %
% --------------------------------------------------------------------- %
let load_more_arithmetic =
let autoload_defs_and_thms thy =
map (\name. autoload_theory(`definition`,thy,name))
(map fst (definitions thy));
map (\name. autoload_theory(`theorem`,thy,name))
(map fst (theorems thy));
()
in
let lib_path = library_pathname() in
\(v:void).
if (mem `more_arithmetic` (ancestry())) then
(print_string `Loading contents of more_arithmetic...`;
print_newline();
let path st = lib_path ^ `/more_arithmetic/` ^ st in
load(path `num_convs`, get_flag_value `print_lib`);
load(path `num_tac`, get_flag_value `print_lib`);
autoload_defs_and_thms `ineq`;
autoload_defs_and_thms `zero_ineq`;
autoload_defs_and_thms `suc`;
autoload_defs_and_thms `add`;
autoload_defs_and_thms `sub`;
autoload_defs_and_thms `pre`;
autoload_defs_and_thms `mult`;
autoload_defs_and_thms `min_max`;
autoload_defs_and_thms `odd_even`;
autoload_defs_and_thms `div_mod`;
delete_cache `ineq`;
delete_cache `zero_ineq`;
delete_cache `suc`;
delete_cache `add`;
delete_cache `sub`;
delete_cache `pre`;
delete_cache `mult`;
delete_cache `min_max`;
delete_cache `odd_even`;
delete_cache `div_mod`;
()) else
failwith `theory more_arithmetic not an ancestor of the current theory`;;
|
