src/HOL/NanoJava/TypeRel.thy
changeset 44013 5cfc1c36ae97
parent 41589 bbd861837ebc
child 44146 8bc84fa57a13
equal deleted inserted replaced
44012:8c1dfd6c2262 44013:5cfc1c36ae97
     2     Author:     David von Oheimb, Technische Universitaet Muenchen
     2     Author:     David von Oheimb, Technische Universitaet Muenchen
     3 *)
     3 *)
     4 
     4 
     5 header "Type relations"
     5 header "Type relations"
     6 
     6 
     7 theory TypeRel imports Decl begin
     7 theory TypeRel imports Decl "~~/src/HOL/Library/Old_Recdef" begin
     8 
     8 
     9 consts
     9 consts
    10   subcls1 :: "(cname \<times> cname) set"  --{* subclass *}
    10   subcls1 :: "(cname \<times> cname) set"  --{* subclass *}
    11 
    11 
    12 abbreviation
    12 abbreviation