Mercurial Mercurial > repos > isabelle / 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.
src/HOL/indrule.ML
changeset 1867 37615e73f2d8
parent 1861 505b104f675a
child 1985 84cf16192e03 
--- 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