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/Complex.thy
changeset 36409 d323e7773aa8
parent 36349 39be26d1bc28
child 36777 be5461582d0f
equal deleted inserted replaced
36350:bc7982c54e37 36409:d323e7773aa8 
    97 
    97 
    98 
    98 
    99 
    99 
   100 subsection {* Multiplication and Division *}
 
   100 subsection {* Multiplication and Division *}
 
   101 
   101 
   102 instantiation complex :: "{field, division_ring_inverse_zero}"
 
   102 instantiation complex :: field_inverse_zero
 
   103 begin
 
   103 begin
 
   104 
   104 
   105 definition
 
   105 definition
 
   106   complex_one_def: "1 = Complex 1 0"
 
   106   complex_one_def: "1 = Complex 1 0"
 
   107 
   107
isabelle