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