author | chaieb |
Mon, 09 Feb 2009 16:57:10 +0000 | |
changeset 29843 | 4bb780545478 |
parent 29842 | 4ac60c7d9b78 |
child 29844 | 4ac95212efcc |
--- a/src/HOL/Library/normarith.ML Mon Feb 09 16:54:03 2009 +0000 +++ b/src/HOL/Library/normarith.ML Mon Feb 09 16:57:10 2009 +0000 @@ -1043,7 +1043,7 @@ then Intfunc.update (v, Rat.neg (Intfunc.apply eq v)) eq else eq; local - val pth_zero = @{thm "Vectors.norm_0"} + val pth_zero = @{thm "norm_0"} val tv_n = (hd o tl o dest_ctyp o ctyp_of_term o dest_arg o dest_arg1 o dest_arg o cprop_of) pth_zero val concl = dest_arg o cprop_of