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