src/LK/LK.thy
changeset 1304 976f9e19a828
parent 1150 66512c9e6bd6
child 1474 3f7d67927fe2
equal deleted inserted replaced
1303:010be89a7541 1304:976f9e19a828
    11 classes term < logic
    11 classes term < logic
    12 
    12 
    13 default term
    13 default term
    14 
    14 
    15 types
    15 types
    16  o sequence seqobj seqcont sequ sobj
    16  o sequence seqobj seqcont sobj
    17 
    17 
    18 arities
    18 arities
    19  o :: logic
    19  o :: logic
    20 
    20 
    21 consts
    21 consts