# HG changeset patch
# User wenzelm
# Date 1343500585 -7200
# Node ID fb446a780d503ca4b9a1a6671de40dabc564b385
# Parent  23456b2a769df87995bd14faca863348f9148356
separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;

diff -r 23456b2a769d -r fb446a780d50 src/HOL/Mirabelle/ex/Ex.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/ex/Ex.thy	Sat Jul 28 20:36:25 2012 +0200
@@ -0,0 +1,12 @@
+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
+
diff -r 23456b2a769d -r fb446a780d50 src/HOL/ROOT
--- a/src/HOL/ROOT	Sat Jul 28 20:27:39 2012 +0200
+++ b/src/HOL/ROOT	Sat Jul 28 20:36:25 2012 +0200
@@ -605,9 +605,9 @@
 session Mirabelle = HOL +
   options [document = false]
   theories Mirabelle_Test
-(* FIXME
-	@cd Library; $(ISABELLE_TOOL) mirabelle -q arith Inner_Product.thy # some arbitrary small test case
-*)
+
+session ex in "Mirabelle/ex" = "HOL-Mirabelle" +
+  theories Ex
 
 session SMT_Examples = "HOL-Word" +
   options [document = false, quick_and_dirty]