src/HOL/Prod.thy
changeset 2886 fd5645efa43d
parent 2880 a0fde30aa126
child 2973 184c7cd8043d
equal deleted inserted replaced
2885:8d229dc0cfe2 2886:fd5645efa43d
    77 
    77 
    78 
    78 
    79 
    79 
    80 (** unit **)
    80 (** unit **)
    81 
    81 
    82 typedef  unit = "{p. p = True}"
    82 typedef  unit = "{True}"
    83 
    83 
    84 consts
    84 consts
    85   "()"          :: unit                           ("'(')")
    85   "()"          :: unit                           ("'(')")
    86 
    86 
    87 defs
    87 defs