Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Wellfounded.thy
changeset 56375 32e0da92c786
parent 56218 1c3f1f2431f9
child 56643 41d3596d8a64 
--- a/src/HOL/Wellfounded.thy	Thu Apr 03 10:51:20 2014 +0200
+++ b/src/HOL/Wellfounded.thy	Thu Apr 03 10:51:22 2014 +0200
@@ -859,7 +859,7 @@
 lemma nat_size [simp, code]: "size (n\<Colon>nat) = n"
   by (induct n) simp_all
 
-declare "prod.size" [no_atp]
+declare prod.size [no_atp]
 
 
 hide_const (open) acc accp
isabelle