src/HOL/Nat.thy
changeset 4104 84433b1ab826
parent 3370 5c5fdce3a4e4
child 4613 67a726003cf8
     1.1 --- a/src/HOL/Nat.thy	Mon Nov 03 21:04:51 1997 +0100
     1.2 +++ b/src/HOL/Nat.thy	Mon Nov 03 21:12:21 1997 +0100
     1.3 @@ -8,6 +8,20 @@
     1.4  
     1.5  Nat = NatDef +
     1.6  
     1.7 +(*install 'automatic' induction tactic, pretending nat is a datatype
     1.8 +  except for induct_tac and exhaust_tac, everything is dummy*)
     1.9 +
    1.10 +MLtext {|
    1.11 +|> Dtype.add_datatype_info
    1.12 +("nat", {case_const = Bound 0, case_rewrites = [],
    1.13 +  constructors = [], induct_tac = nat_ind_tac,
    1.14 +  exhaustion = natE,
    1.15 +  exhaust_tac = fn v => ALLNEWSUBGOALS (res_inst_tac [("n",v)] natE)
    1.16 +                                       (rotate_tac ~1),
    1.17 +  nchotomy = ProtoPure.flexpair_def, case_cong = ProtoPure.flexpair_def})
    1.18 +|}
    1.19 +
    1.20 +
    1.21  instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
    1.22  
    1.23  consts