src/HOL/AxClasses/Tutorial/BoolGroupInsts.thy
changeset 2907 0e272e4c7cb2
parent 1247 18b1441fb603
     1.1 --- a/src/HOL/AxClasses/Tutorial/BoolGroupInsts.thy	Fri Apr 04 16:03:11 1997 +0200
     1.2 +++ b/src/HOL/AxClasses/Tutorial/BoolGroupInsts.thy	Fri Apr 04 16:03:44 1997 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Define overloaded constants "<*>", "inv", "1" on type "bool"
     1.8 +Define overloaded constants "<*>", "inverse", "1" on type "bool"
     1.9  appropriately, then prove that this forms a group.
    1.10  *)
    1.11  
    1.12 @@ -11,9 +11,9 @@
    1.13  (* bool as abelian group *)
    1.14  
    1.15  defs
    1.16 -  prod_bool_def "x <*> y == x ~= (y::bool)"
    1.17 -  inv_bool_def  "inv x   == x::bool"
    1.18 -  unit_bool_def "1       == False"
    1.19 +  prod_bool_def     "x <*> y   == x ~= (y::bool)"
    1.20 +  inverse_bool_def  "inverse x == x::bool"
    1.21 +  unit_bool_def     "1         == False"
    1.22  
    1.23  instance
    1.24    bool :: agroup                {| ALLGOALS (fast_tac HOL_cs) |}