changeset 12305 | 3c3f98b3d9e7 |
parent 12240 | 0760eda193c4 |
child 12799 | 5472afdd3bd3 |
--- a/src/Provers/induct_method.ML Wed Nov 28 00:37:40 2001 +0100 +++ b/src/Provers/induct_method.ML Wed Nov 28 00:38:11 2001 +0100 @@ -182,7 +182,8 @@ [foldr1 (fn (x, x') => [x, x'] MRS Data.conjI) (map (fn x => Drule.implies_elim_list x asms) (th :: ths)) |> Drule.implies_intr_list cprems - |> Drule.standard'] + |> Drule.standard' + |> RuleCases.save th] end;