Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixed theorem reference
authorchaieb
Mon, 09 Feb 2009 16:57:10 +0000
changeset 29843 4bb780545478
parent 29842 4ac60c7d9b78
child 29844 4ac95212efcc
Fixed theorem reference
src/HOL/Library/normarith.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle