changeset 47455 | 26315a545e26 |
parent 46988 | 9f492f5b0cec |
child 59172 | d1c500e0a722 |
--- a/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML Fri Apr 13 13:59:35 2012 +0200 +++ b/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML Fri Apr 13 14:00:26 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Matrix/Compute_Oracle/am_sml.ML +(* Title: HOL/Matrix_LP/Compute_Oracle/am_sml.ML Author: Steven Obua TODO: "parameterless rewrite cannot be used in pattern": In a lot of