src/HOL/Bali/Name.thy
changeset 35431 8758fe1fc9f8
parent 35315 fbdc860d87a3
child 37956 ee939247b2fb
equal deleted inserted replaced
35430:df2862dc23a8 35431:8758fe1fc9f8
    76 
    76 
    77 definition
    77 definition
    78   qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q"
    78   qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q"
    79 
    79 
    80 translations
    80 translations
    81   "mname"  <= "Name.mname"
    81   (type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
    82   "xname"  <= "Name.xname"
       
    83   "tname"  <= "Name.tname"
       
    84   "ename"  <= "Name.ename"
       
    85   "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
       
    86   (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>"
    87 
    83 
    88 
    84 
    89 axiomatization java_lang::pname --{* package java.lang *}
    85 axiomatization java_lang::pname --{* package java.lang *}
    90 
    86