src/HOL/Bali/Basis.thy
changeset 24038 18182c4aec9e
parent 24019 67bde7cfcf10
child 24162 8dfd5dd65d82
     1.1 --- a/src/HOL/Bali/Basis.thy	Sun Jul 29 14:29:51 2007 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Sun Jul 29 14:29:52 2007 +0200
     1.3 @@ -21,11 +21,6 @@
     1.4  declare if_weak_cong [cong del] option.weak_case_cong [cong del]
     1.5  declare length_Suc_conv [iff]
     1.6  
     1.7 -(*###to be phased out *)
     1.8 -ML {*
     1.9 -bind_thm ("make_imp", rearrange_prems [1,0] mp)
    1.10 -*}
    1.11 -
    1.12  lemma Collect_split_eq: "{p. P (split f p)} = {(a,b). P (f a b)}"
    1.13  apply auto
    1.14  done