src/HOL/Typerep.thy
changeset 36176 3fe7e97ccca8
parent 35430 df2862dc23a8
child 38348 cf7b2121ad9d
equal deleted inserted replaced
36175:5cec4ca719d1 36176:3fe7e97ccca8
    88 code_const Typerep
    88 code_const Typerep
    89   (Eval "Term.Type/ (_, _)")
    89   (Eval "Term.Type/ (_, _)")
    90 
    90 
    91 code_reserved Eval Term
    91 code_reserved Eval Term
    92 
    92 
    93 hide (open) const typerep Typerep
    93 hide_const (open) typerep Typerep
    94 
    94 
    95 end
    95 end