src/HOL/List.ML
changeset 10385 22836e4c5f4e
parent 9853 5c6425d83501
child 10709 7a29b71d6352
     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 **)