Theory Ex

theory Ex
imports Pure
theory Ex imports Pure
begin

ML ‹
  val rc = Isabelle_System.bash
    "cd \"$ISABELLE_HOME/src/HOL/Analysis\"; isabelle mirabelle arith Inner_Product.thy";
  if rc <> 0 then error ("Mirabelle example failed: " ^ string_of_int rc)
  else ();
›  "some arbitrary small test case"

end