src/HOL/Matrix_LP/matrixlp.ML
changeset 55413 a8e96847523c
parent 53737 eab25a77af39
child 59582 0fbed69ff081
     1.1 --- a/src/HOL/Matrix_LP/matrixlp.ML	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/Matrix_LP/matrixlp.ML	Wed Feb 12 08:35:56 2014 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  structure MatrixLP : MATRIX_LP =
     1.5  struct
     1.6  
     1.7 -val compute_thms = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_list_case" "ComputeHOL.compute_let"
     1.8 +val compute_thms = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_case_list" "ComputeHOL.compute_let"
     1.9    "ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps"
    1.10    "ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
    1.11    "SparseMatrix.sorted_sp_simps"