CRefine allows users to produce a final file in .tex format that contains
all the refinement steps, as well as the proof obligations, the comments, and the
final code. The comments can be included in the final file before the line it
has be inserted or a list of comments at the end of the file. This output file cab be used
in the generation of a pdf file that provides an excellent visualisation of the
overall refinement.
In order to generate the output file we can click on the button
or choose the Print option in the Development menu.
After selecting Print, a window is shown the user. Using this window, the user must select the development items that must be part of the output file. The user can also choose the format in which the proof obligation must be included: expanded or contracted.
After confirming the selection by clicking on "OK", a dialog box is shown: the user must select the location of the output file and its name. The generated file will be in LaTeX format.
A message will be given at the end of the generation.
In order to generate the output file we can click on the button
or choose the Print option in the Development menu.
After selecting Print, a window is shown the user. Using this window, the user must select the development items that must be part of the output file. The user can also choose the format in which the proof obligation must be included: expanded or contracted.
After confirming the selection by clicking on "OK", a dialog box is shown: the user must select the location of the output file and its name. The generated file will be in LaTeX format.
A message will be given at the end of the generation.