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/Hyperreal/StarClasses.thy
changeset 24742 73b8b42a36b6
parent 24506 020db6ec334a
child 25208 1a7318a04068
equal deleted inserted replaced
24741:a53f5db5acbb 24742:73b8b42a36b6 
   346 instance star :: (semiring_0) semiring_0 
   346 instance star :: (semiring_0) semiring_0 
   347 by intro_classes (transfer, simp)+
 
   347 by intro_classes (transfer, simp)+
 
   348 
   348 
   349 instance star :: (semiring_0_cancel) semiring_0_cancel ..
 
   349 instance star :: (semiring_0_cancel) semiring_0_cancel ..
 
   350 
   350 
   351 instance star :: (comm_semiring) comm_semiring
 
   351 instance star :: (comm_semiring) comm_semiring 
   352 by (intro_classes, transfer, rule distrib)
 
   352 by (intro_classes, transfer, rule left_distrib)
 
   353 
   353 
   354 instance star :: (comm_semiring_0) comm_semiring_0 ..
 
   354 instance star :: (comm_semiring_0) comm_semiring_0 ..
 
   355 instance star :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..
 
   355 instance star :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..
 
   356 
   356 
   357 instance star :: (zero_neq_one) zero_neq_one
 
   357 instance star :: (zero_neq_one) zero_neq_one
isabelle