section‹Standard ML within the Isabelle environment›
theory Examples imports Pure begin
text‹ Isabelle/ML is a somewhat augmented version of Standard ML, with various add-ons that are indispensable for Isabelle development, but may cause conflicts with independent projects in plain Standard ML. The Isabelle/Isar command 🪙‹SML_file›supports official Standard ML within the Isabelle environment, with full support in the Prover IDE (Isabelle/jEdit). Here is a very basic example that defines the factorial function and evaluates it for some arguments. ›
SML_file ‹factorial.sml›
text‹ The subsequent example illustrates the use of multiple 🪙‹SML_file›commands to build larger Standard ML projects. The toplevel SML environment is enriched cumulatively within the theory context of Isabelle --- independently of the Isabelle/ML environment. ›
SML_file ‹Example.sig›
SML_file ‹Example.sml›
text‹ Isabelle/ML and SML share a common run-time system, but the static environments are separate. It is possible to exchange toplevel bindings via separate commands like this. ›
SML_export ‹val f = factorial›🍋‹re-use factorial from SML environment›
ML ‹f 42›
SML_import ‹val println = Output.writeln› 🍋‹re-use Isabelle/ML channel for SML›
SML_import ‹val par_map = Par_List.map› 🍋‹re-use Isabelle/ML parallel list combinator for SML›
end
Messung V0.5 in Prozent
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.16Bemerkung:
(vorverarbeitet am 2026-04-28)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
