Nominal/Ex/LetRec.thy
changeset 3235 5ebd327ffb96
parent 3197 25d11b449e92
child 3236 e2da10806a34
equal deleted inserted replaced
3234:08c3ef07cef7 3235:5ebd327ffb96
    26 thm let_rec.eq_iff
    26 thm let_rec.eq_iff
    27 thm let_rec.fv_bn_eqvt
    27 thm let_rec.fv_bn_eqvt
    28 thm let_rec.size_eqvt
    28 thm let_rec.size_eqvt
    29 
    29 
    30 
    30 
    31 nominal_primrec
    31 nominal_function
    32     height_trm :: "trm \<Rightarrow> nat"
    32     height_trm :: "trm \<Rightarrow> nat"
    33 and height_bp :: "bp \<Rightarrow> nat"
    33 and height_bp :: "bp \<Rightarrow> nat"
    34 where
    34 where
    35   "height_trm (Var x) = 1"
    35   "height_trm (Var x) = 1"
    36 | "height_trm (App l r) = max (height_trm l) (height_trm r)"
    36 | "height_trm (App l r) = max (height_trm l) (height_trm r)"