Up: Interoperability

### 8.1 Isar Interoperability

Aris will scan an Isar proof, which is a proof done using Isabelle, and look for certain keywords.

- fun: The 'fun' keyword.
- type_synonym: The 'type_synonym' keyword.
- lemma/theorem: The 'lemma' keyword.
- case: The 'case' keyword.
- primrec: The 'primrec' keyword.
- definition: The 'definiton' keyword.
- datatype: The 'datatype' keyword.
- class: The 'class' keyword.
- instance: The 'instance' keyword.
- other: Everything else.