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.
Pi_empty1 is a more general simprule than empty_fun
authorpaulson
Mon, 31 Jan 2000 16:13:28 +0100
changeset 8172 988a7737e158
parent 8171 f89329974d2d
child 8173 a9966d5ab84d
Pi_empty1 is a more general simprule than empty_fun
src/ZF/func.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/func.ML	Sun Jan 30 13:24:41 2000 +0100
+++ b/src/ZF/func.ML	Mon Jan 31 16:13:28 2000 +0100
@@ -66,7 +66,7 @@
 by (Blast_tac 1);
 qed "singleton_fun";
 
-Addsimps [empty_fun, singleton_fun];
+Addsimps [Pi_empty1, singleton_fun];
 
 (*** Function Application ***)
isabelle