equal
deleted
inserted
replaced
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)" |