equal
deleted
inserted
replaced
247 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
247 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
248 apply(blast) |
248 apply(blast) |
249 apply(blast) |
249 apply(blast) |
250 done |
250 done |
251 |
251 |
252 termination (eqvt) |
252 nominal_termination (eqvt) |
253 by lexicographic_order |
253 by lexicographic_order |
254 |
254 |
255 nominal_function |
255 nominal_function |
256 nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm" ("_[_\<turnstile>n>_]" [100,100,100] 100) |
256 nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm" ("_[_\<turnstile>n>_]" [100,100,100] 100) |
257 where |
257 where |
441 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
441 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
442 apply(blast) |
442 apply(blast) |
443 apply(blast) |
443 apply(blast) |
444 done |
444 done |
445 |
445 |
446 termination (eqvt) |
446 nominal_termination (eqvt) |
447 by lexicographic_order |
447 by lexicographic_order |
448 |
448 |
449 thm crename.eqvt nrename.eqvt |
449 thm crename.eqvt nrename.eqvt |
450 |
450 |
451 |
451 |