wip

add-links

@@ -23,6 +23,7 @@ arguments:
   coq_mod: coq module that needs to be imported in generated files
 
 effect in the current directory:
+- create a file COMMAND containing the command used to create links
 - create a file BASE containing the base name of hollight_file.ml
 - create a file ROOT_PATH containing the base name of coq_file.v
 - create a file REQUIRING containing the coq modules and root path in the order they are given 
@@ -87,6 +88,11 @@ parse_args() {
     fi
 }
 
+echo create COMMAND ...
+echo '#!/bin/sh' > COMMAND
+echo $0 $* >> COMMAND
+chmod a+x COMMAND
+
 parse_args $*
 if test -n "$requiring" -a -z "$root_path_arg"
 then

erasing.lp

@@ -267,31 +267,31 @@ builtin "axiom_24" ≔ axiom_24;
 
 builtin "Rle" ≔ real_le;
 builtin "real_le_def" ≔ real_le_def;
-builtin "Rdefinitions.Rplus" ≔ real_add;
+builtin "Rplus" ≔ real_add;
 builtin "real_add_def" ≔ real_add_def;
-builtin "Rdefinitions.Rmult" ≔ real_mul;
+builtin "Rmult" ≔ real_mul;
 builtin "real_mul_def" ≔ real_mul_def;
-builtin "Rdefinitions.Rinv" ≔ real_inv;
+builtin "Rinv" ≔ real_inv;
 builtin "real_inv_def" ≔ real_inv_def;
-builtin "Rdefinitions.Ropp" ≔ real_neg;
+builtin "Ropp" ≔ real_neg;
 builtin "real_neg_def" ≔ real_neg_def;
-builtin "Raxioms.INR" ≔ real_of_num;
+builtin "INR" ≔ real_of_num;
 builtin "real_of_num_def" ≔ real_of_num_def;
 builtin "Rpower_nat" ≔ real_pow;
 builtin "real_pow_def" ≔ real_pow_def;
-builtin "Rbasic_fun.Rabs" ≔ real_abs;
+builtin "Rabs" ≔ real_abs;
 builtin "real_abs_def" ≔ real_abs_def;
-builtin "Rdefinitions.Rdiv" ≔ real_div;
+builtin "Rdiv" ≔ real_div;
 builtin "real_div_def" ≔ real_div_def;
-builtin "Rdefinitions.Rminus" ≔ real_sub;
+builtin "Rminus" ≔ real_sub;
 builtin "real_sub_def" ≔ real_sub_def;
-builtin "Rdefinitions.Rge" ≔ real_ge;
+builtin "Rge" ≔ real_ge;
 builtin "real_ge_def" ≔ real_ge_def;
-builtin "Rdefinitions.Rgt" ≔ real_gt;
+builtin "Rgt" ≔ real_gt;
 builtin "real_gt_def" ≔ real_gt_def;
-builtin "Rdefinitions.Rlt" ≔ real_lt;
+builtin "Rlt" ≔ real_lt;
 builtin "real_lt_def" ≔ real_lt_def;
-builtin "Rbasic_fun.Rmax" ≔ real_max;
+builtin "Rmax" ≔ real_max;
 builtin "real_max_def" ≔ real_max_def;
-builtin "Rbasic_fun.Rmin" ≔ real_min;
+builtin "Rmin" ≔ real_min;
 builtin "real_min_def" ≔ real_min_def;