changeset 2680 | 20fa49e610ca |
parent 2608 | 450c9b682a92 |
child 2718 | 460fd0f8d478 |
--- a/src/HOL/NatDef.ML Mon Feb 24 16:12:24 1997 +0100 +++ b/src/HOL/NatDef.ML Tue Feb 25 15:05:14 1997 +0100 @@ -682,3 +682,10 @@ "[| (m::nat) ~= n; m < n ==> P; n < m ==> P |] ==> P" (fn major::prems => [cut_facts_tac [less_linear] 1, REPEAT(eresolve_tac ([disjE,major RS notE]@prems) 1)]); + + + +(* add function nat_add_primrec *) +val (_, nat_add_primrec) = Datatype.add_datatype +([], "nat", [("0", [], Mixfix ("0", [], max_pri)), ("Suc", [dtTyp ([], "nat")], NoSyn)]) HOL.thy; +