Mercurial Mercurial > repos > isabelle / annotate
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/Algebra/abstract/Abstract.thy
author huffman
Sun, 28 Aug 2011 20:56:49 -0700
changeset 44571 bd91b77c4cd6
parent 35849 b5522b51cb1e
permissions -rw-r--r--
move class perfect_space into RealVector.thy; use not_open_singleton as perfect_space class axiom; generalize some lemmas to class perfect_space;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35849
b5522b51cb1e standard headers;
wenzelm
parents: 27541
diff changeset 
     1
 
(*  Author: Clemens Ballarin, started 17 July 1997
b5522b51cb1e standard headers;
wenzelm
parents: 27541
diff changeset 
     2
 












b5522b51cb1e
standard headers;



wenzelm


parents: 
27541

diff
changeset




     3


Summary theory of the development of abstract algebra.








7998






3d0c34795831
Algebra and Polynomial theories, by Clemens Ballarin



paulson


parents: 

diff
changeset




     4


*)













3d0c34795831
Algebra and Polynomial theories, by Clemens Ballarin



paulson


parents: 

diff
changeset




     5









27541






9e585e99b494
tuned import



haftmann


parents: 
16417

diff
changeset




     6


theory Abstract













9e585e99b494
tuned import



haftmann


parents: 
16417

diff
changeset




     7


imports RingHomo Field













9e585e99b494
tuned import



haftmann


parents: 
16417

diff
changeset




     8


begin








13783






3294f727e20d
Fixed term order for normal form in rings.



ballarin


parents: 
7998

diff
changeset




     9














3294f727e20d
Fixed term order for normal form in rings.



ballarin


parents: 
7998

diff
changeset




    10


end















isabelle