diff --git a/@CVC_checker/cvc_check.m b/@CVC_checker/cvc_check.m
index 7cc2e10e31d2b1a3c30cc035a6951246584bd4a5..3cd136013e4420c5f2a9a2a2225af4e81f938bb1 100644
--- a/@CVC_checker/cvc_check.m
+++ b/@CVC_checker/cvc_check.m
@@ -19,10 +19,10 @@ function [ check, seqs ] = cvc_check( object )
 [filename, queries] = object.generate_file;
 
     waitbar(.10,box,'Running Proof');
-tic
+%tic
     % run the cvc command
-[status, result] = system(['cvc3 ' filename ' +model'])
-toc
+[status, result] = system(['cvc3 ' filename ' +model']);
+%toc
 % check return status for errors
 if (status ~= 0)
     
diff --git a/@GUI/GUI.m b/@GUI/GUI.m
index 784d11db82f8b8281905b6cb2388044e258cefc5..40673ba02563c19c3c8bff83b68b326562107367 100644
--- a/@GUI/GUI.m
+++ b/@GUI/GUI.m
@@ -64,7 +64,7 @@ classdef GUI < handle
         multi_opt_out = [];
         prover_opt_pvs = [];
         prover_opt_cvc = [];
-        version = '0.3.1';
+        version = '0.4';
         undo_man = [];
         undo_opt = [];
         redo_opt = [];
diff --git a/@PVS_checker/check_status.m b/@PVS_checker/check_status.m
index 890ee9c48d808fedfb8cca68a51a66e6f2827a46..6093e94bf939b2e1b98f95b515f4168c3a33db68 100644
--- a/@PVS_checker/check_status.m
+++ b/@PVS_checker/check_status.m
@@ -11,7 +11,7 @@
 % Organization: McMaster Centre for Software Certification
 function status = check_status(object)
 script_name = object.generate_pvs_status_script(object.data.function_name );
-[status, result] = system(['pvs -batch -v 3 -l ' script_name])
+[status, result] = system(['pvs -batch -v 3 -l ' script_name]);
 parsed = object.parse_status(result);
 pass = 1;
 if (size(parsed,2) == 0)
diff --git a/@PVS_checker/pvs_check.m b/@PVS_checker/pvs_check.m
index 0833d35773d8ced03f4f24a218196f10d3a13857..5cad2c419fe1d971a4a42f4d09178f4149eca594 100644
--- a/@PVS_checker/pvs_check.m
+++ b/@PVS_checker/pvs_check.m
@@ -52,7 +52,7 @@ if (exists == 1 && (isempty(button) || strcmp(button,'Cancel')))
     output = 'canceled';
     return;
 elseif (exists == 1 && (strcmp(button,'Open PVS')));
-    [status, result] = system(['pvs ' function_name '.pvs'])
+    [status, result] = system(['pvs ' function_name '.pvs']);
     output = 'canceled';
 elseif (exists == 0 || strcmp(button,'Attempt to prove'))
     box = waitbar(0,'Generating Proof Script');
@@ -67,9 +67,9 @@ elseif (exists == 0 || strcmp(button,'Attempt to prove'))
     %---------
     % call pvs in batch mode with script
     % ADD check that pvs actually exists in system
-    tic
-    [status, result] = system(['pvs -batch -v 3 -l ' function_name '.el'])
-    toc
+    %
+    [status, result] = system(['pvs -batch -v 3 -l ' function_name '.el']);
+    %toc
     %objectect.msgbox_scroll(result);
     waitbar(.70,box,'Parsing Results');
     [parsed error] = object.parse_pvs_result(result);
diff --git a/@PVS_checker/pvs_check_for_imports.m b/@PVS_checker/pvs_check_for_imports.m
index 7b4deeb5dd5984695e1d4928a3275c6fe8692f94..8f958c31e2408487d3f9d8fb164649748e0c47e7 100644
--- a/@PVS_checker/pvs_check_for_imports.m
+++ b/@PVS_checker/pvs_check_for_imports.m
@@ -60,7 +60,7 @@ end
 
 for k=1:size(hashtable,2)
     
-    functions = regexp(char(object.data.function_inputs),hashtable{k}(1),'once')
+    functions = regexp(char(object.data.function_inputs),hashtable{k}(1),'once');
             if ~isempty(functions{1})
                 if (~any(ismember(found,hashtable{k}(1))))
                 string = [string 'IMPORTING ' char(hashtable{k}(2)) sprintf('\n')];
diff --git a/html/TT_ug.m b/html/TT_ug.m
index 00116f067d06da67893458138866291dbcabcafe..8c7df3be95868bcc55216db142e5a1fa0b0bd3b0 100644
--- a/html/TT_ug.m
+++ b/html/TT_ug.m
@@ -3,5 +3,7 @@
 % * <TT_ug_opening.html Creating a new Table>
 % * <TT_ug_editing.html Editing a Table>
 % * <TT_ug_checking.html Typechecking a Table>
+% * <TT_ug_floating.html Floating Point Numbers>
 % * <TT_ug_saving.html Saving a Table>
+%
 % Copyright 2010 Colin Eles
\ No newline at end of file
diff --git a/html/TT_ug_floating.m b/html/TT_ug_floating.m
new file mode 100644
index 0000000000000000000000000000000000000000..d37c4f537b6c7a3565f83f0b103863877d67a470
--- /dev/null
+++ b/html/TT_ug_floating.m
@@ -0,0 +1,37 @@
+%% Working with floating point numbers
+%
+%% Floating point numbers
+% One of the limitations with computers is the way that we have to
+% represent real numbers. In a theoretical sense the real numbers has
+% infinite range and infinite precision, however when we want to represent
+% these numbers in a machine using the standard numerical representation
+% for a variety of reasons we
+% lose these properties.
+%
+% Matlab and most computers use the IEEE 754 floating point standard. The
+% standard defines the way real numbers can be represented from the bit
+% level including the results of operations, and exceptions.
+%
+% A full discussion of the standard is beyond the scope of this document we
+% refer the interested reader to <http://www.mathworks.com/help/techdoc/matlab_prog/f2-12135.html Matlab's documentation> as well as the
+% <http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4610935&tag=1
+% standard documentation>
+%
+%% Proving tables with floating point numbers
+%
+% The toolbox has support for proving tables with floating point inputs.
+% Currently only PVS is supported for this feature, and in general manual
+% intervention with the prover will likely be required.
+%
+% Several new types are provided which can be used as anyother type in the input and output fields.
+% 
+% 
+% * single - a finite or infinite single precision number
+% * single_finite - a finite single precision number
+% * double - a finite or infinite double precision number
+% * double_finite - a finite double precision number
+%
+% A sample input string might be "x:double_finite, y:double_finite". The
+% same rules for subtyping still apply, as it may be necessary to subtype
+% inputs in order to get them to typecheck properly.
+%
\ No newline at end of file
diff --git a/html/html/TT_ug.html b/html/html/TT_ug.html
index 30dafd5bdb71ca31dfa0e4e6db13970e039ae3fb..e46cfa9c63d99fd649abc41ae7def5069ddcb30b 100644
--- a/html/html/TT_ug.html
+++ b/html/html/TT_ug.html
@@ -6,7 +6,7 @@
    <!--
 This HTML is auto-generated from an M-file.
 To make changes, update the M-file and republish this document.
-      --><title>User Guide</title><meta name="generator" content="MATLAB 7.10"><meta name="date" content="2010-11-25"><meta name="m-file" content="TT_ug"><style type="text/css">
+      --><title>User Guide</title><meta name="generator" content="MATLAB 7.10"><meta name="date" content="2011-04-14"><meta name="m-file" content="TT_ug"><style type="text/css">
 
 body {
   background-color: white;
@@ -62,15 +62,16 @@ p.footer {
   color: gray;
 }
 
-  </style></head><body><div class="content"><h1>User Guide</h1><div><ul><li><a href="TT_ug_background.html">Tabular Expressions</a></li><li><a href="TT_ug_opening.html">Creating a new Table</a></li><li><a href="TT_ug_editing.html">Editing a Tabular Expression</a></li><li><a href="TT_ug_checking.html">Typechecking a Table</a></li></ul></div><p>Copyright 2010 Colin Eles</p><p class="footer"><br>
+  </style></head><body><div class="content"><h1>User Guide</h1><div><ul><li><a href="TT_ug_opening.html">Creating a new Table</a></li><li><a href="TT_ug_editing.html">Editing a Table</a></li><li><a href="TT_ug_checking.html">Typechecking a Table</a></li><li><a href="TT_ug_floating.html">Floating Point Numbers</a></li><li><a href="TT_ug_saving.html">Saving a Table</a></li></ul></div><p>Copyright 2010 Colin Eles</p><p class="footer"><br>
       Published with MATLAB&reg; 7.10<br></p></div><!--
 ##### SOURCE BEGIN #####
 %% User Guide
 %
-% * <TT_ug_background.html Tabular Expressions>
 % * <TT_ug_opening.html Creating a new Table>
-% * <TT_ug_editing.html Editing a Tabular Expression>
+% * <TT_ug_editing.html Editing a Table>
 % * <TT_ug_checking.html Typechecking a Table>
+% * <TT_ug_floating.html Floating Point Numbers>
+% * <TT_ug_saving.html Saving a Table>
 %
 % Copyright 2010 Colin Eles
 ##### SOURCE END #####
diff --git a/html/html/TT_ug_floating.html b/html/html/TT_ug_floating.html
new file mode 100644
index 0000000000000000000000000000000000000000..3b1a5422f25a24f855cc4336928b2cc40bcacd8e
--- /dev/null
+++ b/html/html/TT_ug_floating.html
@@ -0,0 +1,103 @@
+
+<!DOCTYPE html
+  PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
+<html><head>
+      <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
+   <!--
+This HTML is auto-generated from an M-file.
+To make changes, update the M-file and republish this document.
+      --><title>Working with floating point numbers</title><meta name="generator" content="MATLAB 7.10"><meta name="date" content="2011-04-12"><meta name="m-file" content="TT_ug_floating"><style type="text/css">
+
+body {
+  background-color: white;
+  margin:10px;
+}
+
+h1 {
+  color: #990000; 
+  font-size: x-large;
+}
+
+h2 {
+  color: #990000;
+  font-size: medium;
+}
+
+/* Make the text shrink to fit narrow windows, but not stretch too far in 
+wide windows. */ 
+p,h1,h2,div.content div {
+  max-width: 600px;
+  /* Hack for IE6 */
+  width: auto !important; width: 600px;
+}
+
+pre.codeinput {
+  background: #EEEEEE;
+  padding: 10px;
+}
+@media print {
+  pre.codeinput {word-wrap:break-word; width:100%;}
+} 
+
+span.keyword {color: #0000FF}
+span.comment {color: #228B22}
+span.string {color: #A020F0}
+span.untermstring {color: #B20000}
+span.syscmd {color: #B28C00}
+
+pre.codeoutput {
+  color: #666666;
+  padding: 10px;
+}
+
+pre.error {
+  color: red;
+}
+
+p.footer {
+  text-align: right;
+  font-size: xx-small;
+  font-weight: lighter;
+  font-style: italic;
+  color: gray;
+}
+
+  </style></head><body><div class="content"><h1>Working with floating point numbers</h1><!--introduction--><!--/introduction--><h2>Contents</h2><div><ul><li><a href="#1">Floating point numbers</a></li><li><a href="#2">Proving tables with floating point numbers</a></li></ul></div><h2>Floating point numbers<a name="1"></a></h2><p>One of the limitations with computers is the way that we have to represent real numbers. In a theoretical sense the real numbers has infinite range and infinite precision, however when we want to represent these numbers in a machine using the standard numerical representation for a variety of reasons we lose these properties.</p><p>Matlab and most computers use the IEEE 754 floating point standard. The standard defines the way real numbers can be represented from the bit level including the results of operations, and exceptions.</p><p>A full discussion of the standard is beyond the scope of this document we refer the interested reader to <a href="http://www.mathworks.com/help/techdoc/matlab_prog/f2-12135.html">Matlab's documentation</a> as well as the <a href="http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4610935&amp;tag=1">standard documentation</a></p><h2>Proving tables with floating point numbers<a name="2"></a></h2><p>The toolbox has support for proving tables with floating point inputs. Currently only PVS is supported for this feature, and in general manual intervention with the prover will likely be required.</p><p>Several new types are provided which can be used as anyother type in the input and output fields.</p><div><ul><li>single - a finite or infinite single precision number</li><li>single_finite - a finite single precision number</li><li>double - a finite or infinite double precision number</li><li>double_finite - a finite double precision number</li></ul></div><p class="footer"><br>
+      Published with MATLAB&reg; 7.10<br></p></div><!--
+##### SOURCE BEGIN #####
+%% Working with floating point numbers
+%
+%% Floating point numbers
+% One of the limitations with computers is the way that we have to
+% represent real numbers. In a theoretical sense the real numbers has
+% infinite range and infinite precision, however when we want to represent
+% these numbers in a machine using the standard numerical representation
+% for a variety of reasons we
+% lose these properties.
+%
+% Matlab and most computers use the IEEE 754 floating point standard. The
+% standard defines the way real numbers can be represented from the bit
+% level including the results of operations, and exceptions.
+%
+% A full discussion of the standard is beyond the scope of this document we
+% refer the interested reader to <http://www.mathworks.com/help/techdoc/matlab_prog/f2-12135.html Matlab's documentation> as well as the
+% <http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4610935&tag=1
+% standard documentation>
+%
+%% Proving tables with floating point numbers
+%
+% The toolbox has support for proving tables with floating point inputs.
+% Currently only PVS is supported for this feature, and in general manual
+% intervention with the prover will likely be required.
+%
+% Several new types are provided which can be used as anyother type in the input and output fields.
+% 
+% 
+% * single - a finite or infinite single precision number
+% * single_finite - a finite single precision number
+% * double - a finite or infinite double precision number
+% * double_finite - a finite double precision number
+%
+%
+##### SOURCE END #####
+--></body></html>
\ No newline at end of file