equal
  deleted
  inserted
  replaced
  
    
    
|      1 (*  Title:      Tools/Compute_Oracle/am_sml.ML |      1 (*  Title:      HOL/Matrix/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.  |