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.
in_set_butlast_appendI supersedes in_set_butlast_appendI1,2
authorpaulson
Thu, 10 Sep 1998 17:28:36 +0200
changeset 5458 0e26af5975ba
parent 5457 367878234bb2
child 5459 1dbaf888f4e7
in_set_butlast_appendI supersedes in_set_butlast_appendI1,2
src/HOL/Lex/RegSet_of_nat_DA.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Thu Sep 10 17:27:50 1998 +0200
+++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Thu Sep 10 17:28:36 1998 +0200
@@ -4,8 +4,8 @@
     Copyright   1998 TUM
 *)
 
-Addsimps [in_set_butlast_appendI1,in_set_butlast_appendI2];
-AddIs    [in_set_butlast_appendI1,in_set_butlast_appendI2];
+Addsimps [in_set_butlast_appendI];
+AddIs    [in_set_butlast_appendI];
 Addsimps [image_eqI];
 
 (* Lists *)
isabelle