diff -r 9bbf2a1f9b3f -r 2293711213dd Paper/Paper.thy --- a/Paper/Paper.thy Wed Mar 31 12:30:17 2010 +0200 +++ b/Paper/Paper.thy Wed Mar 31 15:20:58 2010 +0200 @@ -1479,10 +1479,13 @@ obtain by simple calculations the equalities. \end{proof} - With the above equations we can substitute free variables for support in - the lifted free variable equations, which gives us the support equations - for the term constructors. With this we can show that for each binding in - a constructors the bindings can be renamed. +%%% Without defining permute_bn, we cannot even write the substitution +%%% of bindings in term constructors... + +% With the above equations we can substitute free variables for support in +% the lifted free variable equations, which gives us the support equations +% for the term constructors. With this we can show that for each binding in +% a constructors the bindings can be renamed. *}