src/HOL/Mirabelle/ex/Ex.thy
author wenzelm
Sat, 23 May 2015 17:19:37 +0200
changeset 60299 5ae2a2e74c93
parent 48589 fb446a780d50
child 62573 27f90319a499
permissions -rw-r--r--
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;

theory Ex imports Pure
begin

ML {*
  val rc = Isabelle_System.bash
    "cd \"$ISABELLE_HOME/src/HOL/Library\"; \"$ISABELLE_TOOL\" mirabelle -q arith Inner_Product.thy";
  if rc <> 0 then error ("Mirabelle example failed: " ^ string_of_int rc)
  else ();
*} -- "some arbitrary small test case"

end