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.
fixed name;
authorwenzelm
Wed, 30 Aug 2000 14:02:12 +0200
changeset 9741 0502f06c2d29
parent 9740 1c5b0f27de56
child 9742 98d3ca2c18f7
fixed name;
NEWS file | annotate | diff | comparison | revisions 
--- a/NEWS	Wed Aug 30 13:55:26 2000 +0200
+++ b/NEWS	Wed Aug 30 14:02:12 2000 +0200
@@ -281,8 +281,8 @@
 
 * HOL: theorems impI, allI, ballI bound as "strip";
 
-* new function rulify: thm -> thm for turning outer -->/! into ==>/?; behaves
-like eq_spec_mp;
+* new function rulify: thm -> thm for turning outer -->/! into ==>/?;
+behaves like qed_spec_mp;
 
 * theory Sexp now in HOL/Induct examples (it used to be part of main
 HOL, but was unused);
isabelle