Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
deleted a redundant bind_thm
authorpaulson
Wed, 28 Jun 2000 10:41:16 +0200
changeset 9161 cee6d5aee7c8
parent 9160 7a98dbf3e579
child 9162 647d554a65ae
deleted a redundant bind_thm
src/HOL/Set.ML file | annotate | diff | comparison | revisions 
--- 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);
isabelle