This directory contains examples of how the CF tactics can be used.
cf_examplesScript.sml: A collection of small examples that show (and test) what can be done in CF proofs.
cf_tutorialScript.sml: A small tutorial on how to do proofs in CF using the tools provided by CakeML's support for CF reasoning.