src/HOL/AxClasses/Tutorial/Sigs.thy
changeset 1247 18b1441fb603
child 2907 0e272e4c7cb2
equal deleted inserted replaced
1246:706cfddca75c 1247:18b1441fb603
       
     1 (*  Title:      HOL/AxClasses/Tutorial/Sigs.thy
       
     2     ID:         $Id$
       
     3     Author:     Markus Wenzel, TU Muenchen
       
     4 
       
     5 Some polymorphic constants for the 'signature' parts of axclasses.
       
     6 *)
       
     7 
       
     8 Sigs = HOL +
       
     9 
       
    10 consts
       
    11   "<*>"         :: "['a, 'a] => 'a"             (infixl 70)
       
    12   "inv"         :: "'a => 'a"
       
    13   "1"           :: "'a"                         ("1")
       
    14 
       
    15 end