| changeset 56255 | 968667bbb8d2 |
| parent 54489 | 03ff4d1e6784 |
| child 58889 | 5b7a9633cfa8 |
--- a/src/HOL/Matrix_LP/ComputeFloat.thy Sat Mar 22 18:19:57 2014 +0100 +++ b/src/HOL/Matrix_LP/ComputeFloat.thy Sat Mar 22 19:33:39 2014 +0100 @@ -239,6 +239,6 @@ lemmas arith = arith_simps rel_simps diff_nat_numeral nat_0 nat_neg_numeral powerarith floatarith not_false_eq_true not_true_eq_false -ML_file "~~/src/HOL/Tools/float_arith.ML" +ML_file "float_arith.ML" end