src/HOL/NatDef.ML
changeset 3292 8b143c196d42
parent 3282 c31e6239d4c9
child 3308 da002cef7090
     1.1 --- a/src/HOL/NatDef.ML	Thu May 22 12:59:08 1997 +0200
     1.2 +++ b/src/HOL/NatDef.ML	Thu May 22 13:05:52 1997 +0200
     1.3 @@ -70,10 +70,12 @@
     1.4  qed "natE";
     1.5  
     1.6  (*Install 'automatic' induction tactic, pretending nat is a datatype *)
     1.7 -(*except for induct_tac, everything is dummy*)
     1.8 +(*except for induct_tac and exhaust_tac, everything is dummy*)
     1.9  datatypes := [("nat",{case_const = Bound 0, case_rewrites = [],
    1.10    constructors = [], induct_tac = nat_ind_tac,
    1.11 -  exhaustion = natE, exhaust_tac = fn v => res_inst_tac [("n",v)] natE,
    1.12 +  exhaustion = natE,
    1.13 +  exhaust_tac = fn v => ALLNEWSUBGOALS (res_inst_tac [("n",v)] natE)
    1.14 +                                       (rotate_tac ~1),
    1.15    nchotomy = flexpair_def, case_cong = flexpair_def})];
    1.16  
    1.17