# HG changeset patch
# User haftmann
# Date 1191519969 -7200
# Node ID 0fc73c4003ac44f6d6be79857c29152680c57c72
# Parent  2bdf31a97362c411a47e4fe0aaf2af1bf8ba26e4
added illustrative diagnostics

diff -r 2bdf31a97362 -r 0fc73c4003ac src/HOL/ex/Classpackage.thy
--- a/src/HOL/ex/Classpackage.thy	Thu Oct 04 19:42:03 2007 +0200
+++ b/src/HOL/ex/Classpackage.thy	Thu Oct 04 19:46:09 2007 +0200
@@ -293,6 +293,8 @@
 end
 
 (*FIXME*)
+thm (no_abbrevs) pow_def
+thm (no_abbrevs) pow_def [folded monoid_class.npow]
 lemmas pow_def [code func] = pow_def [folded monoid_class.npow]
 
 context group begin