src/HOL/Wellfounded.thy
changeset 56375 32e0da92c786
parent 56218 1c3f1f2431f9
child 56643 41d3596d8a64
     1.1 --- a/src/HOL/Wellfounded.thy	Thu Apr 03 10:51:20 2014 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Thu Apr 03 10:51:22 2014 +0200
     1.3 @@ -859,7 +859,7 @@
     1.4  lemma nat_size [simp, code]: "size (n\<Colon>nat) = n"
     1.5    by (induct n) simp_all
     1.6  
     1.7 -declare "prod.size" [no_atp]
     1.8 +declare prod.size [no_atp]
     1.9  
    1.10  
    1.11  hide_const (open) acc accp