Mercurial Mercurial > repos > isabelle / comparison
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/ex/Classpackage.thy
changeset 24843 0fc73c4003ac
parent 24657 185502d54c3d
child 24914 95cda5dd58d5
equal deleted inserted replaced
24842:2bdf31a97362 24843:0fc73c4003ac 
   291     else (npow (nat k) x))"
 
   291     else (npow (nat k) x))"
 
   292 
   292 
   293 end
 
   293 end
 
   294 
   294 
   295 (*FIXME*)
 
   295 (*FIXME*)
 
       
   296 thm (no_abbrevs) pow_def
 
       
   297 thm (no_abbrevs) pow_def [folded monoid_class.npow]
 
   296 lemmas pow_def [code func] = pow_def [folded monoid_class.npow]
 
   298 lemmas pow_def [code func] = pow_def [folded monoid_class.npow]
 
   297 
   299 
   298 context group begin
 
   300 context group begin
 
   299 
   301 
   300 abbreviation
 
   302 abbreviation
isabelle