src/Tools/SML/Examples.thy

merged DERIV_intros, has_derivative_intros into derivative_intros

(*  Title:      Tools/SML/Examples.thy
    Author:     Makarius
*)

header {* 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"

end