rev_exhaust: rulify;
authorwenzelm
Fri Nov 03 21:32:41 2000 +0100 (2000-11-03)
changeset 1038522836e4c5f4e
parent 10384 a499b9ce2ffe
child 10386 581a5a143994
rev_exhaust: rulify;
src/HOL/List.ML
     1.1 --- a/src/HOL/List.ML	Fri Nov 03 21:31:53 2000 +0100
     1.2 +++ b/src/HOL/List.ML	Fri Nov 03 21:32:41 2000 +0100
     1.3 @@ -417,8 +417,9 @@
     1.4  Goal  "(xs = [] --> P) -->  (!ys y. xs = ys@[y] --> P) --> P";
     1.5  by (rev_induct_tac "xs" 1);
     1.6  by Auto_tac;
     1.7 -bind_thm ("rev_exhaust",
     1.8 -  impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
     1.9 +qed "rev_exhaust_aux";
    1.10 +
    1.11 +bind_thm ("rev_exhaust", Rulify.rulify rev_exhaust_aux);
    1.12  
    1.13  
    1.14  (** set **)