1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Mirabelle/ex/Ex.thy	Sat Jul 28 20:36:25 2012 +0200
     1.3 @@ -0,0 +1,12 @@
     1.4 +theory Ex imports Pure
     1.5 +begin
     1.6 +
     1.7 +ML {*
     1.8 +  val rc = Isabelle_System.bash
     1.9 +    "cd \"$ISABELLE_HOME/src/HOL/Library\"; \"$ISABELLE_TOOL\" mirabelle -q arith Inner_Product.thy";
    1.10 +  if rc <> 0 then error ("Mirabelle example failed: " ^ string_of_int rc)
    1.11 +  else ();
    1.12 +*} -- "some arbitrary small test case"
    1.13 +
    1.14 +end
    1.15 +

     2.1 --- a/src/HOL/ROOT	Sat Jul 28 20:27:39 2012 +0200
     2.2 +++ b/src/HOL/ROOT	Sat Jul 28 20:36:25 2012 +0200
     2.3 @@ -605,9 +605,9 @@
     2.4  session Mirabelle = HOL +
     2.5    options [document = false]
     2.6    theories Mirabelle_Test
     2.7 -(* FIXME
     2.8 -	@cd Library; $(ISABELLE_TOOL) mirabelle -q arith Inner_Product.thy # some arbitrary small test case
     2.9 -*)
    2.10 +
    2.11 +session ex in "Mirabelle/ex" = "HOL-Mirabelle" +
    2.12 +  theories Ex
    2.13  
    2.14  session SMT_Examples = "HOL-Word" +
    2.15    options [document = false, quick_and_dirty]