| changeset 1180 | 3f36936f1280 |
| parent 1178 | 275a1cb3f2ba |
| child 1185 | 7566b899ca6a |
| 1179:789fbba5c23f | 1180:3f36936f1280 |
|---|---|
89 snd (Primrec.add_primrec |
89 snd (Primrec.add_primrec |
90 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs lthy) |
90 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs lthy) |
91 end |
91 end |
92 *} |
92 *} |
93 |
93 |
94 |
94 (* test |
95 atom_decl name |
95 atom_decl name |
96 |
96 |
97 datatype rtrm1 = |
97 datatype rtrm1 = |
98 rVr1 "name" |
98 rVr1 "name" |
99 | rAp1 "rtrm1" "rtrm1" |
99 | rAp1 "rtrm1" "rtrm1" |
116 local_setup {* define_raw_fv "Fv.rtrm1" |
116 local_setup {* define_raw_fv "Fv.rtrm1" |
117 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]], |
117 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]], |
118 [[], [[]], [[], []]]] *} |
118 [[], [[]], [[], []]]] *} |
119 print_theorems |
119 print_theorems |
120 |
120 |
121 *) |
|
122 |
|
121 end |
123 end |