src/HOL/Bali/Name.thy
changeset 38540 8c08631cb4b6
parent 37956 ee939247b2fb
child 58249 180f1b3508ed
equal deleted inserted replaced
38539:3be65f879bcd 38540:8c08631cb4b6
    73 instance ..
    73 instance ..
    74 
    74 
    75 end
    75 end
    76 
    76 
    77 definition
    77 definition
    78   qtname_qtname_def: "qtname (q::'a qtname_ext_type) = q"
    78   qtname_qtname_def: "qtname (q::'a qtname_scheme) = q"
    79 
    79 
    80 translations
    80 translations
    81   (type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
    81   (type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
    82   (type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
    82   (type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
    83 
    83