src/LCF/LCF.thy
changeset 35128 c1ad622e90e4
parent 27239 f2f42f9fa09d
child 35762 af3ff2ba4c54
equal deleted inserted replaced
35127:5b29c1660047 35128:c1ad622e90e4
    17 classes cpo < "term"
    17 classes cpo < "term"
    18 defaultsort cpo
    18 defaultsort cpo
    19 
    19 
    20 typedecl tr
    20 typedecl tr
    21 typedecl void
    21 typedecl void
    22 typedecl ('a,'b) "*"    (infixl 6)
    22 typedecl ('a,'b) "*"    (infixl "*" 6)
    23 typedecl ('a,'b) "+"    (infixl 5)
    23 typedecl ('a,'b) "+"    (infixl "+" 5)
    24 
    24 
    25 arities
    25 arities
    26   "fun" :: (cpo, cpo) cpo
    26   "fun" :: (cpo, cpo) cpo
    27   "*" :: (cpo, cpo) cpo
    27   "*" :: (cpo, cpo) cpo
    28   "+" :: (cpo, cpo) cpo
    28   "+" :: (cpo, cpo) cpo