equal
deleted
inserted
replaced
30 apply (simp add: fresh_Pair) |
30 apply (simp add: fresh_Pair) |
31 apply (simp add: eqvt_at_def) |
31 apply (simp add: eqvt_at_def) |
32 apply (simp add: flip_fresh_fresh) |
32 apply (simp add: flip_fresh_fresh) |
33 done |
33 done |
34 |
34 |
35 termination (eqvt) by lexicographic_order |
35 nominal_termination (eqvt) by lexicographic_order |
36 |
36 |
37 nominal_function |
37 nominal_function |
38 ccomp :: "cpsctxt => cpsctxt => cpsctxt" |
38 ccomp :: "cpsctxt => cpsctxt => cpsctxt" |
39 where |
39 where |
40 "ccomp Hole C = C" |
40 "ccomp Hole C = C" |
55 apply (simp add: fresh_Pair) |
55 apply (simp add: fresh_Pair) |
56 apply (simp add: eqvt_at_def) |
56 apply (simp add: eqvt_at_def) |
57 apply (simp add: flip_fresh_fresh) |
57 apply (simp add: flip_fresh_fresh) |
58 done |
58 done |
59 |
59 |
60 termination (eqvt) by lexicographic_order |
60 nominal_termination (eqvt) by lexicographic_order |
61 |
61 |
62 nominal_function |
62 nominal_function |
63 CPSv :: "lt => lt" |
63 CPSv :: "lt => lt" |
64 and CPS :: "lt => cpsctxt" where |
64 and CPS :: "lt => cpsctxt" where |
65 "CPSv (Var x) = x~" |
65 "CPSv (Var x) = x~" |