# HG changeset patch
# User berghofe
# Date 1197977184 -3600
# Node ID 5226396bf26159fd9f6d783d2677ba157d54114c
# Parent  4853eeb031584eb6371e3b8933eb172e51d27619
Renamed *.size to prod.size.

diff -r 4853eeb03158 -r 5226396bf261 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Dec 18 12:26:00 2007 +0100
+++ b/src/HOL/Nat.thy	Tue Dec 18 12:26:24 2007 +0100
@@ -1152,7 +1152,7 @@
 lemma size_bool [code func]:
   "size (b\<Colon>bool) = 0" by (cases b) auto
 
-declare "*.size" [noatp]
+declare "prod.size" [noatp]
 
 
 subsection {* Embedding of the Naturals into any