120 |
120 |
121 val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; |
121 val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; |
122 val terms = thms >> map Drule.dest_term; |
122 val terms = thms >> map Drule.dest_term; |
123 in |
123 in |
124 |
124 |
125 val attribute = |
125 val ferrak_setup = |
126 (keyword minfN |-- thms) |
126 Attrib.setup @{binding ferrack} |
|
127 ((keyword minfN |-- thms) |
127 -- (keyword pinfN |-- thms) |
128 -- (keyword pinfN |-- thms) |
128 -- (keyword nmiN |-- thms) |
129 -- (keyword nmiN |-- thms) |
129 -- (keyword npiN |-- thms) |
130 -- (keyword npiN |-- thms) |
130 -- (keyword lin_denseN |-- thms) |
131 -- (keyword lin_denseN |-- thms) |
131 -- (keyword qeN |-- thms) |
132 -- (keyword qeN |-- thms) |
132 -- (keyword atomsN |-- terms) >> |
133 -- (keyword atomsN |-- terms) >> |
133 (fn ((((((minf,pinf),nmi),npi),lin_dense),qe), atoms)=> |
134 (fn ((((((minf,pinf),nmi),npi),lin_dense),qe), atoms)=> |
134 if length qe = 1 then |
135 if length qe = 1 then |
135 add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense, |
136 add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense, |
136 qe = hd qe, atoms = atoms}, |
137 qe = hd qe, atoms = atoms}, |
137 {isolate_conv = undefined, whatis = undefined, simpset = HOL_ss}) |
138 {isolate_conv = undefined, whatis = undefined, simpset = HOL_ss}) |
138 else error "only one theorem for qe!") |
139 else error "only one theorem for qe!")) |
|
140 "Ferrante Rackoff data"; |
139 |
141 |
140 end; |
142 end; |
141 |
143 |
142 |
144 |
143 (* theory setup *) |
145 (* theory setup *) |
144 |
146 |
145 val setup = Attrib.setup @{binding ferrack} attribute "Ferrante Rackoff data"; |
147 val setup = ferrak_setup; |
146 |
148 |
147 end; |
149 end; |