Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Real/HahnBanach/FunctionOrder.thy
changeset 11472 d08d4e17a5f6
parent 10687 c186279eecea
child 13515 a6a7025fd7e8 
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Tue Aug 07 19:29:08 2001 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Tue Aug 07 21:27:00 2001 +0200
@@ -27,7 +27,7 @@
   "graph F f \<equiv> {(x, f x) | x. x \<in> F}"
 
 lemma graphI [intro?]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f"
-  by (unfold graph_def, intro CollectI exI) blast
+  by (unfold graph_def) blast
 
 lemma graphI2 [intro?]: "x \<in> F \<Longrightarrow> \<exists>t\<in> (graph F f). t = (x, f x)"
   by (unfold graph_def) blast
isabelle