function nat_add_primrec added to allow primrec definitions over nat
authorpusch
Tue Feb 25 15:05:14 1997 +0100 (1997-02-25)
changeset 268020fa49e610ca
parent 2679 3eac428cdd1b
child 2681 93ed51a91622
function nat_add_primrec added to allow primrec definitions over nat
src/HOL/NatDef.ML
     1.1 --- a/src/HOL/NatDef.ML	Mon Feb 24 16:12:24 1997 +0100
     1.2 +++ b/src/HOL/NatDef.ML	Tue Feb 25 15:05:14 1997 +0100
     1.3 @@ -682,3 +682,10 @@
     1.4    "[| (m::nat) ~= n; m < n ==> P; n < m ==> P |] ==> P"
     1.5    (fn major::prems => [cut_facts_tac [less_linear] 1,
     1.6                         REPEAT(eresolve_tac ([disjE,major RS notE]@prems) 1)]);
     1.7 +
     1.8 +
     1.9 +
    1.10 +(* add function nat_add_primrec *) 
    1.11 +val (_, nat_add_primrec) = Datatype.add_datatype
    1.12 +([], "nat", [("0", [], Mixfix ("0", [], max_pri)), ("Suc", [dtTyp ([], "nat")], NoSyn)]) HOL.thy;
    1.13 +