src/HOL/Nat.thy
changeset 4613 67a726003cf8
parent 4104 84433b1ab826
child 4640 ac6cf9f18653
equal deleted inserted replaced
4612:26764de50c74 4613:67a726003cf8
    14 MLtext {|
    14 MLtext {|
    15 |> Dtype.add_datatype_info
    15 |> Dtype.add_datatype_info
    16 ("nat", {case_const = Bound 0, case_rewrites = [],
    16 ("nat", {case_const = Bound 0, case_rewrites = [],
    17   constructors = [], induct_tac = nat_ind_tac,
    17   constructors = [], induct_tac = nat_ind_tac,
    18   exhaustion = natE,
    18   exhaustion = natE,
    19   exhaust_tac = fn v => ALLNEWSUBGOALS (res_inst_tac [("n",v)] natE)
    19   exhaust_tac = fn v => (res_inst_tac [("n",v)] natE)
    20                                        (rotate_tac ~1),
    20                         THEN_ALL_NEW (rotate_tac ~1),
    21   nchotomy = ProtoPure.flexpair_def, case_cong = ProtoPure.flexpair_def})
    21   nchotomy = ProtoPure.flexpair_def, case_cong = ProtoPure.flexpair_def})
    22 |}
    22 |}
    23 
    23 
    24 
    24 
    25 instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
    25 instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)