deleted a redundant bind_thm
authorpaulson
Wed Jun 28 10:41:16 2000 +0200 (2000-06-28)
changeset 9161cee6d5aee7c8
parent 9160 7a98dbf3e579
child 9162 647d554a65ae
deleted a redundant bind_thm
src/HOL/Set.ML
     1.1 --- a/src/HOL/Set.ML	Wed Jun 28 10:40:06 2000 +0200
     1.2 +++ b/src/HOL/Set.ML	Wed Jun 28 10:41:16 2000 +0200
     1.3 @@ -19,8 +19,6 @@
     1.4  by (Asm_full_simp_tac 1);
     1.5  qed "CollectD";
     1.6  
     1.7 -bind_thm ("CollectE", make_elim CollectD);
     1.8 -
     1.9  val [prem] = Goal "[| !!x. (x:A) = (x:B) |] ==> A = B";
    1.10  by (rtac (prem RS ext RS arg_cong RS box_equals) 1);
    1.11  by (rtac Collect_mem_eq 1);