equal
deleted
inserted
replaced
63 |
63 |
64 (*** Inductive definition of the PR functions ***) |
64 (*** Inductive definition of the PR functions ***) |
65 |
65 |
66 structure Primrec = Inductive_Fun |
66 structure Primrec = Inductive_Fun |
67 (val thy = Primrec0.thy |
67 (val thy = Primrec0.thy |
|
68 val thy_name = "Primrec" |
68 val rec_doms = [("primrec", "list(nat)->nat")] |
69 val rec_doms = [("primrec", "list(nat)->nat")] |
69 val sintrs = |
70 val sintrs = |
70 ["SC : primrec", |
71 ["SC : primrec", |
71 "k: nat ==> CONST(k) : primrec", |
72 "k: nat ==> CONST(k) : primrec", |
72 "i: nat ==> PROJ(i) : primrec", |
73 "i: nat ==> PROJ(i) : primrec", |