src/HOLCF/IOA/meta_theory/Sequence.thy
changeset 36452 d37c6eed8117
parent 35907 ea0bf2a01eb0
child 36458 031e90da9720
equal deleted inserted replaced
36451:ddc965e172c4 36452:d37c6eed8117
     6 
     6 
     7 theory Sequence
     7 theory Sequence
     8 imports Seq
     8 imports Seq
     9 begin
     9 begin
    10 
    10 
    11 defaultsort type
    11 default_sort type
    12 
    12 
    13 types 'a Seq = "'a::type lift seq"
    13 types 'a Seq = "'a::type lift seq"
    14 
    14 
    15 consts
    15 consts
    16 
    16