changeset 63971 | da89140186e2 |
parent 63167 | 0909deb8059b |
child 67443 | 3abf6a722518 |
--- a/src/HOL/Mirabelle/ex/Ex.thy Fri Sep 30 15:35:32 2016 +0200 +++ b/src/HOL/Mirabelle/ex/Ex.thy Fri Sep 30 15:35:37 2016 +0200 @@ -3,7 +3,7 @@ ML \<open> val rc = Isabelle_System.bash - "cd \"$ISABELLE_HOME/src/HOL/Library\"; isabelle mirabelle arith Inner_Product.thy"; + "cd \"$ISABELLE_HOME/src/HOL/Analysis\"; isabelle mirabelle arith Inner_Product.thy"; if rc <> 0 then error ("Mirabelle example failed: " ^ string_of_int rc) else (); \<close> \<comment> "some arbitrary small test case"