changeset 10385 | 22836e4c5f4e |
parent 9853 | 5c6425d83501 |
child 10709 | 7a29b71d6352 |
--- a/src/HOL/List.ML Fri Nov 03 21:31:53 2000 +0100 +++ b/src/HOL/List.ML Fri Nov 03 21:32:41 2000 +0100 @@ -417,8 +417,9 @@ Goal "(xs = [] --> P) --> (!ys y. xs = ys@[y] --> P) --> P"; by (rev_induct_tac "xs" 1); by Auto_tac; -bind_thm ("rev_exhaust", - impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp))))); +qed "rev_exhaust_aux"; + +bind_thm ("rev_exhaust", Rulify.rulify rev_exhaust_aux); (** set **)