src/HOL/ex/Classpackage.thy
changeset 22424 8a5412121687
parent 22384 33a46e6c7f04
child 22473 753123c89d72
     1.1 --- a/src/HOL/ex/Classpackage.thy	Fri Mar 09 08:45:53 2007 +0100
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Fri Mar 09 08:45:55 2007 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Florian Haftmann, TU Muenchen
     1.5  *)
     1.6  
     1.7 -header {* Test and examples for new class package *}
     1.8 +header {* Test and examples for Isar class package *}
     1.9  
    1.10  theory Classpackage
    1.11  imports Main
    1.12 @@ -328,6 +328,7 @@
    1.13  instance * :: (group_comm, group_comm) group_comm
    1.14  by default (simp_all add: split_paired_all mult_prod_def comm)
    1.15  
    1.16 + 
    1.17  definition
    1.18    "X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, [a, b] \<otimes> \<one> \<otimes> [a, b, c])"
    1.19  definition