changeset 62573 | 27f90319a499 |
parent 48589 | fb446a780d50 |
child 62589 | b5783412bfed |
--- a/src/HOL/Mirabelle/ex/Ex.thy Wed Mar 09 16:53:14 2016 +0100 +++ b/src/HOL/Mirabelle/ex/Ex.thy Wed Mar 09 19:30:09 2016 +0100 @@ -3,7 +3,7 @@ ML {* val rc = Isabelle_System.bash - "cd \"$ISABELLE_HOME/src/HOL/Library\"; \"$ISABELLE_TOOL\" mirabelle -q arith Inner_Product.thy"; + "cd \"$ISABELLE_HOME/src/HOL/Library\"; \"$ISABELLE_TOOL\" mirabelle arith Inner_Product.thy"; if rc <> 0 then error ("Mirabelle example failed: " ^ string_of_int rc) else (); *} -- "some arbitrary small test case"