corrected comment
authorpaulson
Tue Jul 16 15:48:27 1996 +0200 (1996-07-16)
changeset 186737615e73f2d8
parent 1866 a1a41b4b02e7
child 1868 836950047d85
corrected comment
src/HOL/indrule.ML
     1.1 --- a/src/HOL/indrule.ML	Tue Jul 16 15:47:07 1996 +0200
     1.2 +++ b/src/HOL/indrule.ML	Tue Jul 16 15:48:27 1996 +0200
     1.3 @@ -185,7 +185,7 @@
     1.4             rewrite_goals_tac all_defs  THEN
     1.5             simp_tac (mut_ss addsimps [Part_def]) 1  THEN
     1.6             IF_UNSOLVED (*simp_tac may have finished it off!*)
     1.7 -             ((*simplify assumptions, but don't accept new rewrite rules!*)
     1.8 +             ((*simplify assumptions*)
     1.9                full_simp_tac mut_ss 1  THEN
    1.10                (*unpackage and use "prem" in the corresponding place*)
    1.11                REPEAT (rtac impI 1)  THEN