Up: Interoperability [Contents]
Aris will scan an Isar proof, which is a proof done using Isabelle, and look for certain keywords. This is still being tested, and doesn’t work fully yet. This section will be updated as more of this is implemented.
| • 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. |