Quot/Examples/IntEx.thy
changeset 652 d8f07b5bcfae
parent 648 830b58c2fa94
child 656 c86a47d4966e
equal deleted inserted replaced
649:0b29650e3fd8 652:d8f07b5bcfae
   319 apply simp
   319 apply simp
   320 done
   320 done
   321 
   321 
   322 lemma "map (\<lambda>x. PLUS x ZERO) l = l"
   322 lemma "map (\<lambda>x. PLUS x ZERO) l = l"
   323 apply(lifting lam_tst4)
   323 apply(lifting lam_tst4)
   324 done
   324 apply(cleaning)
       
   325 sorry
   325 
   326 
   326 end
   327 end