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.
corrected comment
authorpaulson
Tue, 16 Jul 1996 15:48:27 +0200
changeset 1867 37615e73f2d8
parent 1866 a1a41b4b02e7
child 1868 836950047d85
corrected comment
src/HOL/indrule.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/indrule.ML	Tue Jul 16 15:47:07 1996 +0200
+++ b/src/HOL/indrule.ML	Tue Jul 16 15:48:27 1996 +0200
@@ -185,7 +185,7 @@
            rewrite_goals_tac all_defs  THEN
            simp_tac (mut_ss addsimps [Part_def]) 1  THEN
            IF_UNSOLVED (*simp_tac may have finished it off!*)
-             ((*simplify assumptions, but don't accept new rewrite rules!*)
+             ((*simplify assumptions*)
               full_simp_tac mut_ss 1  THEN
               (*unpackage and use "prem" in the corresponding place*)
               REPEAT (rtac impI 1)  THEN
isabelle