The setup involves installing the following required software tools and libraries on your computer :

- Mathematica 9.0.
- Eclipse SDK version 3.5.2.
- Ocaml 3.09.0 and HOL Light related to this version of Ocaml.
- XML-Light 2.0.

Additional requirement : 
- Copy the link to JLINK  (JLink.jar) in the directory where Mathematica is installed
 (Path_to_Wolfram_directory/Wolfram/Mathematica/9.0/SystemFiles/JLink) 

- Update the JLink.jar in the Java application "OpenMath-Mathematica-Phrasebook.zip". In our implementation, we use the OpenMath-Mathematica phrasebook proposed by Caprotti et al. [1,2] :
	* Open Eclipse. 
	* Go to the "Refrenced Libraries" in the "Package Explorer" panel in Eclispe.
	* Click on the JLink.jar and paste the new path of the JLink jar file.

- Generate a Runnable Jar file of the Whole Java application : 
	* Go to buttom "File" in the eclispe tool. 
	* Do the following : Export -> java -> Runnable JAR file ->select the path of your directory -> finish. 

- Update the path for the Jar file of the Java application in the "mathematicaphrasebook.ml" in your HOL Light directory.



To compile these files:
 
 1) Extract the Zip files : "HolLight-Mathematica.zip" in you HOL Light directory.


 2) Start HOL Light, i.e., cd to your HOL Light directory, start ocaml,
   and load the file "hol.ml":

   > cd /hol/light/directory
   > ocaml
     Objective Caml version 3.09.0

   # #use "hol.ml";;


  Remark: this should take a couple of minutes.

2) From inside the HOL Light session, load the following:

    # #use  "main.ml";;   



3) Running Examples, load the following:  


   # call_mathematica "(x pow 2) + x + &1 > (x pow 2) + x + &2 " "Simplify";;

   # call_mathematica "diff ((sin x + x - (cos x) + (x pow 2)), x)" "Simplify";; 

   # call_mathematica "int ((x pow 2 + x - &1), x)" "Simplify";; 

   # call_mathematica "(x pow 2) + x + &1 > (x pow 2) + x + &2 " "Simplify";;

   # call_mathematica "x pow 3 + &2 * (x pow 2) + x " "Factor";;

   # call_mathematica "x pow 2 - &1 = &0" "Solve";;


References

  [1] O. Caprotti, A. M. Cohen, and M. Riem. JAVA Phrasebooks for Computer Algebra and Automated Deduction. SIGSAM Bulltin, 34:33–37, 2000.
 

  [2] Source Code of the Phrasebook Mathematica-OpenMath. http://mathdox.org/new-web/index.html.