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 {* |
62 termination (eqvt) by lexicographic_order |
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 |
63 |
|
64 thm height_trm_height_bp.eqvt |
71 |
65 |
72 thm height_trm_def height_bp_def |
|
73 |
|
74 termination (eqvt) by lexicographic_order |
|
75 |
66 |
76 end |
67 end |
77 |
68 |
78 |
69 |
79 |
70 |