equal
deleted
inserted
replaced
57 apply(simp add: eqvt_at_def) |
57 apply(simp add: eqvt_at_def) |
58 apply(perm_simp) |
58 apply(perm_simp) |
59 apply (simp add: permute_fun_def) |
59 apply (simp add: permute_fun_def) |
60 done |
60 done |
61 |
61 |
|
62 ML {* |
|
63 let |
|
64 val [t1, t2] = Item_Net.content (Nominal_Function_Common.get_function @{context}) |
|
65 in |
|
66 (#eqvts (snd t1), |
|
67 #eqvts (snd t2)) |
|
68 end |
|
69 *} |
|
70 |
|
71 |
62 thm height_trm_def height_bp_def |
72 thm height_trm_def height_bp_def |
63 |
73 |
64 termination (eqvt) by lexicographic_order |
74 termination (eqvt) by lexicographic_order |
65 |
75 |
66 end |
76 end |