Mercurial Mercurial > hg > nominal2 / 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.
Quot/QuotScript.thy
changeset 893 1fc2b6f6ea2a
parent 891 7bac7dffadeb
child 908 1bf4337919d3 
--- a/Quot/QuotScript.thy	Fri Jan 15 15:56:06 2010 +0100
+++ b/Quot/QuotScript.thy	Fri Jan 15 15:56:25 2010 +0100
@@ -301,8 +301,6 @@
   done
 
 lemma bex_reg_eqv_range:
-  fixes P::"'a \<Rightarrow> bool"
-  and x::"'a"
   assumes a: "equivp R2"
   shows   "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"
   apply(auto)
nominal2