Up: Interoperability [Contents]

10.1 Isar Interoperability

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.

AltStyle によって変換されたページ (->オリジナル) /