# HG changeset patch
# User haftmann
# Date 1328915248 -3600
# Node ID 460b0d81d4864590bd946b60ffa5f691c27c1084
# Parent  c7c289ce9ad28d79346e8b4846144163c0fa312d
brute-force adjustion

diff -r c7c289ce9ad2 -r 460b0d81d486 src/HOL/Matrix/matrixlp.ML
--- a/src/HOL/Matrix/matrixlp.ML	Sat Feb 11 00:06:48 2012 +0100
+++ b/src/HOL/Matrix/matrixlp.ML	Sat Feb 11 00:07:28 2012 +0100
@@ -16,8 +16,8 @@
 val compute_thms = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_list_case" "ComputeHOL.compute_let"
   "ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps"
   "ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
-  "SparseMatrix.sorted_sp_simps" "ComputeNumeral.number_norm"
-  "ComputeNumeral.natnorm"};
+  "SparseMatrix.sorted_sp_simps"
+  "ComputeNumeral.natnorm"}; (*"ComputeNumeral.number_norm"*)
 
 val spm_mult_le_dual_prts_no_let_real = @{thm "spm_mult_le_dual_prts_no_let" [where ?'a = real]}