| changeset 37591 | d3daea901123 |
| parent 35700 | 951974ce903e |
| child 39302 | d7728f65b353 |
--- a/src/HOL/Library/Nat_Bijection.thy Mon Jun 28 15:03:07 2010 +0200 +++ b/src/HOL/Library/Nat_Bijection.thy Mon Jun 28 15:03:07 2010 +0200 @@ -213,6 +213,7 @@ termination list_decode apply (relation "measure id", simp_all) apply (drule arg_cong [where f="prod_encode"]) +apply (drule sym) apply (simp add: le_imp_less_Suc le_prod_encode_2) done