/Isabelle-CAS-Integration

A project to integrate the functionality of Computer Algebra Systems into Isabelle

Primary LanguageIsabelle

Isabelle-CAS-Integration

Developed from the dissertations of Thomas Hickman and Christian Pardillo Laursen.

Steps for installation

OR

  • Install SageMath and optionally FriCAS.

  • Add the file config.sml configures the path of the file sage-integration/ConvertToIsabelle.py. An example of this file is found in config-example.sml.

  • Finally, launch Isabelle/jEdit with the ODE theory loading, to avoid recompiling. This can be done with the command isabelle jedit -d ~/AFP/thys -l Ordinary_Differential_Equations, replacing the path to the AFP with wherever it is downloaded.

Usage

Examples can be found in the two test sets: Keymaera_tests.thy and TestSet.thy.