tuned document;
authorwenzelm
Sun Mar 03 16:00:14 2019 +0100 (3 months ago ago)
changeset 7003660b924cda764
parent 70035 cc0b3e177b49
child 70037 bb41977edb7e
tuned document;
src/HOL/Isar_Examples/Group.thy
     1.1 --- a/src/HOL/Isar_Examples/Group.thy	Fri Mar 01 21:29:59 2019 +0100
     1.2 +++ b/src/HOL/Isar_Examples/Group.thy	Sun Mar 03 16:00:14 2019 +0100
     1.3 @@ -12,8 +12,8 @@
     1.4  
     1.5  text \<open>
     1.6    Groups over signature \<open>(* :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>, 1 :: \<alpha>, inverse :: \<alpha> \<Rightarrow> \<alpha>)\<close> are
     1.7 -  defined as an axiomatic type class as follows. Note that the parent class
     1.8 -  \<open>times\<close> is provided by the basic HOL theory.
     1.9 +  defined as an axiomatic type class as follows. Note that the parent classes
    1.10 +  \<^class>\<open>times\<close>, \<^class>\<open>one\<close>, \<^class>\<open>inverse\<close> is provided by the basic HOL theory.
    1.11  \<close>
    1.12  
    1.13  class group = times + one + inverse +