author | wenzelm |
Thu, 21 Jun 2007 15:42:09 +0200 | |
changeset 23455 | e18a371624b5 |
permissions | -rw-r--r-- |
23455
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/ferrante_rackoff_data.ML |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
3 |
Author: Amine Chaieb, TU Muenchen |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
4 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
5 |
Context data for Ferrante and Rackoff's algorithm for quantifier |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
6 |
elimination in dense linear orders. |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
7 |
*) |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
8 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
9 |
signature FERRANTE_RACKOF_DATA = |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
10 |
sig |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
11 |
datatype ord = Lt | Le | Gt | Ge | Eq | NEq | Nox |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
12 |
type entry |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
13 |
val get: Proof.context -> (thm * entry) list |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
14 |
val del: attribute |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
15 |
val add: entry -> attribute |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
16 |
val funs: thm -> |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
17 |
{isolate_conv: morphism -> Proof.context -> cterm list -> cterm -> thm, |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
18 |
whatis: morphism -> cterm -> cterm -> ord, |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
19 |
simpset: morphism -> simpset} |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
20 |
-> morphism -> Context.generic -> Context.generic |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
21 |
val match: Proof.context -> cterm -> entry option |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
22 |
val setup: theory -> theory |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
23 |
end; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
24 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
25 |
structure Ferrante_Rackoff_Data: FERRANTE_RACKOF_DATA = |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
26 |
struct |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
27 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
28 |
(* data *) |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
29 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
30 |
datatype ord = Lt | Le | Gt | Ge | Eq | NEq | Nox |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
31 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
32 |
type entry = |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
33 |
{minf: thm list, pinf: thm list, nmi: thm list, npi: thm list, |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
34 |
ld: thm list, qe: thm, atoms : cterm list} * |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
35 |
{isolate_conv: Proof.context -> cterm list -> cterm -> thm, |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
36 |
whatis : cterm -> cterm -> ord, |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
37 |
simpset : simpset}; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
38 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
39 |
val eq_key = Thm.eq_thm; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
40 |
fun eq_data arg = eq_fst eq_key arg; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
41 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
42 |
structure Data = GenericDataFun |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
43 |
( |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
44 |
type T = (thm * entry) list; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
45 |
val empty = []; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
46 |
val extend = I; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
47 |
fun merge _ = AList.merge eq_key (K true); |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
48 |
); |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
49 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
50 |
val get = Data.get o Context.Proof; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
51 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
52 |
fun del_data key = remove eq_data (key, []); |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
53 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
54 |
val del = Thm.declaration_attribute (Data.map o del_data); |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
55 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
56 |
fun undefined x = error "undefined"; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
57 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
58 |
fun add entry = |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
59 |
Thm.declaration_attribute (fn key => fn context => context |> Data.map |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
60 |
(del_data key #> cons (key, entry))); |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
61 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
62 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
63 |
(* extra-logical functions *) |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
64 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
65 |
fun funs raw_key {isolate_conv = icv, whatis = wi, simpset = ss} phi = Data.map (fn data => |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
66 |
let |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
67 |
val key = Morphism.thm phi raw_key; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
68 |
val _ = AList.defined eq_key data key orelse |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
69 |
raise THM ("No data entry for structure key", 0, [key]); |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
70 |
val fns = {isolate_conv = icv phi, whatis = wi phi, simpset = ss phi}; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
71 |
in AList.map_entry eq_key key (apsnd (K fns)) data end); |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
72 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
73 |
fun match ctxt tm = |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
74 |
let |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
75 |
fun match_inst |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
76 |
({minf, pinf, nmi, npi, ld, qe, atoms}, |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
77 |
fns as {isolate_conv, whatis, simpset}) pat = |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
78 |
let |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
79 |
fun h instT = |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
80 |
let |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
81 |
val substT = Thm.instantiate (instT, []); |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
82 |
val substT_cterm = Drule.cterm_rule substT; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
83 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
84 |
val minf' = map substT minf |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
85 |
val pinf' = map substT pinf |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
86 |
val nmi' = map substT nmi |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
87 |
val npi' = map substT npi |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
88 |
val ld' = map substT ld |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
89 |
val qe' = substT qe |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
90 |
val atoms' = map substT_cterm atoms |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
91 |
val result = ({minf = minf', pinf = pinf', nmi = nmi', npi = npi', |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
92 |
ld = ld', qe = qe', atoms = atoms'}, fns) |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
93 |
in SOME result end |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
94 |
in (case try Thm.match (pat, tm) of |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
95 |
NONE => NONE |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
96 |
| SOME (instT, _) => h instT) |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
97 |
end; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
98 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
99 |
fun match_struct (_, |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
100 |
entry as ({atoms = atoms, ...}, _): entry) = |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
101 |
get_first (match_inst entry) atoms; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
102 |
in get_first match_struct (get ctxt) end; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
103 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
104 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
105 |
(* concrete syntax *) |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
106 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
107 |
local |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
108 |
val minfN = "minf"; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
109 |
val pinfN = "pinf"; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
110 |
val nmiN = "nmi"; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
111 |
val npiN = "npi"; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
112 |
val lin_denseN = "lindense"; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
113 |
val qeN = "qe" |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
114 |
val atomsN = "atoms" |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
115 |
val simpsN = "simps" |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
116 |
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
117 |
val any_keyword = |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
118 |
keyword minfN || keyword pinfN || keyword nmiN |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
119 |
|| keyword npiN || keyword lin_denseN || keyword qeN |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
120 |
|| keyword atomsN || keyword simpsN; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
121 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
122 |
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
123 |
val terms = thms >> map Drule.dest_term; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
124 |
in |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
125 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
126 |
fun att_syntax src = src |> Attrib.syntax |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
127 |
((keyword minfN |-- thms) |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
128 |
-- (keyword pinfN |-- thms) |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
129 |
-- (keyword nmiN |-- thms) |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
130 |
-- (keyword npiN |-- thms) |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
131 |
-- (keyword lin_denseN |-- thms) |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
132 |
-- (keyword qeN |-- thms) |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
133 |
-- (keyword atomsN |-- terms) >> |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
134 |
(fn ((((((minf,pinf),nmi),npi),lin_dense),qe), atoms)=> |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
135 |
if length qe = 1 then |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
136 |
add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense, |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
137 |
qe = hd qe, atoms = atoms}, |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
138 |
{isolate_conv = undefined, whatis = undefined, simpset = HOL_ss}) |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
139 |
else error "only one theorem for qe!")) |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
140 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
141 |
end; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
142 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
143 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
144 |
(* theory setup *) |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
145 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
146 |
val setup = |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
147 |
Attrib.add_attributes [("dlo", att_syntax, "Ferrante Rackoff data")]; |
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
148 |
|
e18a371624b5
Context data for Ferrante-Rackoff quantifier elimination.
wenzelm
parents:
diff
changeset
|
149 |
end; |