This commit fixes the declaration of the uabsfuns, i.e. the xi_0 and
xi_1 terms in the corres theorems. These are now declared as Isabelle
constants, which users can overload later on whilst theorems using these
constants will still remain true.
One minor fix is fixing the make file for the system-abstract-verif
example. It now copies the typing table to a file that Isabelle expects
to exist.
This commit fixes the declaration of the uabsfuns, i.e. the xi_0 and xi_1 terms in the corres theorems. These are now declared as Isabelle constants, which users can overload later on whilst theorems using these constants will still remain true.
One minor fix is fixing the make file for the system-abstract-verif example. It now copies the typing table to a file that Isabelle expects to exist.