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