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]