changeset 9161 | cee6d5aee7c8 |
parent 9108 | 9fff97d29837 |
child 9186 | 7b2f4e6538b4 |
--- a/src/HOL/Set.ML Wed Jun 28 10:40:06 2000 +0200 +++ b/src/HOL/Set.ML Wed Jun 28 10:41:16 2000 +0200 @@ -19,8 +19,6 @@ by (Asm_full_simp_tac 1); qed "CollectD"; -bind_thm ("CollectE", make_elim CollectD); - val [prem] = Goal "[| !!x. (x:A) = (x:B) |] ==> A = B"; by (rtac (prem RS ext RS arg_cong RS box_equals) 1); by (rtac Collect_mem_eq 1);