equal
deleted
inserted
replaced
1 (* Title: HOL/Matrix/Compute_Oracle/am_sml.ML |
1 (* Title: HOL/Matrix_LP/Compute_Oracle/am_sml.ML |
2 Author: Steven Obua |
2 Author: Steven Obua |
3 |
3 |
4 TODO: "parameterless rewrite cannot be used in pattern": In a lot of |
4 TODO: "parameterless rewrite cannot be used in pattern": In a lot of |
5 cases it CAN be used, and these cases should be handled |
5 cases it CAN be used, and these cases should be handled |
6 properly; right now, all cases raise an exception. |
6 properly; right now, all cases raise an exception. |