1 (* Title: HOL/Tools/meson.ML
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Copyright 1992 University of Cambridge
6 The MESON resolution proof procedure for HOL.
8 When making clauses, avoids using the rewriter -- instead uses RS recursively
10 NEED TO SORT LITERALS BY # OF VARS, USING ==>I/E. ELIMINATES NEED FOR
11 FUNCTION nodups -- if done to goal clauses too!
14 signature BASIC_MESON =
16 val size_of_subgoals : thm -> int
17 val make_cnf : thm list -> thm -> thm list
18 val make_nnf : thm -> thm
19 val make_nnf1 : thm -> thm
20 val skolemize : thm -> thm
21 val make_clauses : thm list -> thm list
22 val make_horns : thm list -> thm list
23 val best_prolog_tac : (thm -> int) -> thm list -> tactic
24 val depth_prolog_tac : thm list -> tactic
25 val gocls : thm list -> thm list
26 val skolemize_prems_tac : thm list -> int -> tactic
27 val MESON : (thm list -> tactic) -> int -> tactic
28 val best_meson_tac : (thm -> int) -> int -> tactic
29 val safe_best_meson_tac : int -> tactic
30 val depth_meson_tac : int -> tactic
31 val prolog_step_tac' : thm list -> int -> tactic
32 val iter_deepen_prolog_tac : thm list -> tactic
33 val iter_deepen_meson_tac : thm list -> int -> tactic
34 val meson_tac : int -> tactic
35 val negate_head : thm -> thm
36 val select_literal : int -> thm -> thm
37 val skolemize_tac : int -> tactic
38 val make_clauses_tac : int -> tactic
39 val check_is_fol_term : term -> term
46 val not_conjD = thm "meson_not_conjD";
47 val not_disjD = thm "meson_not_disjD";
48 val not_notD = thm "meson_not_notD";
49 val not_allD = thm "meson_not_allD";
50 val not_exD = thm "meson_not_exD";
51 val imp_to_disjD = thm "meson_imp_to_disjD";
52 val not_impD = thm "meson_not_impD";
53 val iff_to_disjD = thm "meson_iff_to_disjD";
54 val not_iffD = thm "meson_not_iffD";
55 val conj_exD1 = thm "meson_conj_exD1";
56 val conj_exD2 = thm "meson_conj_exD2";
57 val disj_exD = thm "meson_disj_exD";
58 val disj_exD1 = thm "meson_disj_exD1";
59 val disj_exD2 = thm "meson_disj_exD2";
60 val disj_assoc = thm "meson_disj_assoc";
61 val disj_comm = thm "meson_disj_comm";
62 val disj_FalseD1 = thm "meson_disj_FalseD1";
63 val disj_FalseD2 = thm "meson_disj_FalseD2";
65 val depth_limit = ref 2000;
67 (**** Operators for forward proof ****)
69 (*Like RS, but raises Option if there are no unifiers and allows multiple unifiers.*)
70 fun resolve1 (tha,thb) = Seq.hd (biresolution false [(false,tha)] 1 thb);
72 (*raises exception if no rules apply -- unlike RL*)
73 fun tryres (th, rls) =
74 let fun tryall [] = raise THM("tryres", 0, th::rls)
75 | tryall (rl::rls) = (resolve1(th,rl) handle Option.Option => tryall rls)
78 (*Permits forward proof from rules that discharge assumptions*)
79 fun forward_res nf st =
80 case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st)
82 | NONE => raise THM("forward_res", 0, [st]);
85 (*Are any of the logical connectives in "bs" present in the term?*)
87 let fun has (Const(a,_)) = false
88 | has (Const("Trueprop",_) $ p) = has p
89 | has (Const("Not",_) $ p) = has p
90 | has (Const("op |",_) $ p $ q) = member (op =) bs "op |" orelse has p orelse has q
91 | has (Const("op &",_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q
92 | has (Const("All",_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p
93 | has (Const("Ex",_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p
98 (**** Clause handling ****)
100 fun literals (Const("Trueprop",_) $ P) = literals P
101 | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
102 | literals (Const("Not",_) $ P) = [(false,P)]
103 | literals P = [(true,P)];
105 (*number of literals in a term*)
106 val nliterals = length o literals;
109 (*** Tautology Checking ***)
111 fun signed_lits_aux (Const ("op |", _) $ P $ Q) (poslits, neglits) =
112 signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
113 | signed_lits_aux (Const("Not",_) $ P) (poslits, neglits) = (poslits, P::neglits)
114 | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
116 fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
118 (*Literals like X=X are tautologous*)
119 fun taut_poslit (Const("op =",_) $ t $ u) = t aconv u
120 | taut_poslit (Const("True",_)) = true
121 | taut_poslit _ = false;
124 let val (poslits,neglits) = signed_lits th
125 in exists taut_poslit poslits
127 exists (member (op aconv) neglits) (HOLogic.false_const :: poslits)
129 handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*)
132 (*** To remove trivial negated equality literals from clauses ***)
134 (*They are typically functional reflexivity axioms and are the converses of
135 injectivity equivalences*)
137 val not_refl_disj_D = thm"meson_not_refl_disj_D";
139 (*Is either term a Var that does not properly occur in the other term?*)
140 fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u))
141 | eliminable (u, t as Var _) = t aconv u orelse not (Logic.occs(t,u))
142 | eliminable _ = false;
144 fun refl_clause_aux 0 th = th
145 | refl_clause_aux n th =
146 case HOLogic.dest_Trueprop (concl_of th) of
147 (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) =>
148 refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*)
149 | (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) =>
151 then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*)
152 else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*)
153 | (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
154 | _ => (*not a disjunction*) th;
156 fun notequal_lits_count (Const ("op |", _) $ P $ Q) =
157 notequal_lits_count P + notequal_lits_count Q
158 | notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1
159 | notequal_lits_count _ = 0;
161 (*Simplify a clause by applying reflexivity to its negated equality literals*)
163 let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th))
164 in zero_var_indexes (refl_clause_aux neqs th) end
165 handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*)
168 (*** The basic CNF transformation ***)
170 (*Estimate the number of clauses in order to detect infeasible theorems*)
171 fun nclauses (Const("Trueprop",_) $ t) = nclauses t
172 | nclauses (Const("op &",_) $ t $ u) = nclauses t + nclauses u
173 | nclauses (Const("Ex", _) $ Abs (_,_,t)) = nclauses t
174 | nclauses (Const("All",_) $ Abs (_,_,t)) = nclauses t
175 | nclauses (Const("op |",_) $ t $ u) = nclauses t * nclauses u
176 | nclauses _ = 1; (* literal *)
178 (*Replaces universally quantified variables by FREE variables -- because
179 assumptions may not contain scheme variables. Later, call "generalize". *)
181 let val newname = gensym "A_"
182 val spec' = read_instantiate [("x", newname)] spec
185 (*Used with METAHYPS below. There is one assumption, which gets bound to prem
186 and then normalized via function nf. The normal form is given to resolve_tac,
187 presumably to instantiate a Boolean variable.*)
188 fun resop nf [prem] = resolve_tac (nf prem) 1;
191 exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "prop"]);
193 (*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
194 Strips universal quantifiers and breaks up conjunctions.
195 Eliminates existential quantifiers using skoths: Skolemization theorems.*)
196 fun cnf skoths (th,ths) =
197 let fun cnf_aux (th,ths) =
198 if has_meta_conn (prop_of th) then ths (*meta-level: ignore*)
199 else if not (has_conns ["All","Ex","op &"] (prop_of th))
200 then th::ths (*no work to do, terminate*)
201 else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
202 Const ("op &", _) => (*conjunction*)
203 cnf_aux (th RS conjunct1,
204 cnf_aux (th RS conjunct2, ths))
205 | Const ("All", _) => (*universal quantifier*)
206 cnf_aux (freeze_spec th, ths)
208 (*existential quantifier: Insert Skolem functions*)
209 cnf_aux (tryres (th,skoths), ths)
210 | Const ("op |", _) => (*disjunction*)
212 (METAHYPS (resop cnf_nil) 1) THEN
213 (fn st' => st' |> METAHYPS (resop cnf_nil) 1)
214 in Seq.list_of (tac (th RS disj_forward)) @ ths end
215 | _ => (*no work to do*) th::ths
216 and cnf_nil th = cnf_aux (th,[])
218 if nclauses (concl_of th) > 20
219 then (Output.debug ("cnf is ignoring: " ^ string_of_thm th); ths)
220 else cnf_aux (th,ths)
223 (*Convert all suitable free variables to schematic variables,
224 but don't discharge assumptions.*)
225 fun generalize th = Thm.varifyT (forall_elim_vars 0 (forall_intr_frees th));
227 fun make_cnf skoths th =
228 filter (not o is_taut)
229 (map (refl_clause o generalize) (cnf skoths (th, [])));
232 (**** Removal of duplicate literals ****)
234 (*Forward proof, passing extra assumptions as theorems to the tactic*)
235 fun forward_res2 nf hyps st =
238 (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
241 | NONE => raise THM("forward_res2", 0, [st]);
243 (*Remove duplicates in P|Q by assuming ~P in Q
244 rls (initially []) accumulates assumptions of the form P==>False*)
245 fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
246 handle THM _ => tryres(th,rls)
247 handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
248 [disj_FalseD1, disj_FalseD2, asm_rl])
251 (*Remove duplicate literals, if there are any*)
253 if null(findrep(literals(prop_of th))) then th
254 else nodups_aux [] th;
257 (**** Generation of contrapositives ****)
259 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
260 fun assoc_right th = assoc_right (th RS disj_assoc)
263 (*Must check for negative literal first!*)
264 val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
266 (*For ordinary resolution. *)
267 val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule'];
269 (*Create a goal or support clause, conclusing False*)
270 fun make_goal th = (*Must check for negative literal first!*)
271 make_goal (tryres(th, clause_rules))
272 handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]);
274 (*Sort clauses by number of literals*)
275 fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
277 fun sort_clauses ths = sort (make_ord fewerlits) ths;
279 (*True if the given type contains bool anywhere*)
280 fun has_bool (Type("bool",_)) = true
281 | has_bool (Type(_, Ts)) = exists has_bool Ts
282 | has_bool _ = false;
284 (*Is the string the name of a connective? It doesn't matter if this list is
285 incomplete, since when actually called, the only connectives likely to
286 remain are & | Not.*)
287 val is_conn = member (op =)
288 ["Trueprop", "op &", "op |", "op -->", "op =", "Not",
289 "All", "Ex", "Ball", "Bex"];
291 (*True if the term contains a function where the type of any argument contains
293 val has_bool_arg_const =
295 (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
297 (*Raises an exception if any Vars in the theorem mention type bool; they
298 could cause make_horn to loop! Also rejects functions whose arguments are
299 Booleans or other functions.*)
301 not (exists (has_bool o fastype_of) (term_vars t) orelse
302 not (Term.is_first_order ["all","All","Ex"] t) orelse
303 has_bool_arg_const t orelse
306 (*FIXME: replace this by the boolean-valued version above!*)
307 fun check_is_fol_term t =
308 if is_fol_term t then t else raise TERM("check_is_fol_term",[t]);
310 fun check_is_fol th = (check_is_fol_term (prop_of th); th);
313 (*Create a meta-level Horn clause*)
314 fun make_horn crules th = make_horn crules (tryres(th,crules))
317 (*Generate Horn clauses for all contrapositives of a clause. The input, th,
318 is a HOL disjunction.*)
319 fun add_contras crules (th,hcs) =
320 let fun rots (0,th) = hcs
321 | rots (k,th) = zero_var_indexes (make_horn crules th) ::
322 rots(k-1, assoc_right (th RS disj_comm))
323 in case nliterals(prop_of th) of
325 | n => rots(n, assoc_right th)
328 (*Use "theorem naming" to label the clauses*)
329 fun name_thms label =
330 let fun name1 (th, (k,ths)) =
331 (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths)
333 in fn ths => #2 (foldr name1 (length ths, []) ths) end;
335 (*Is the given disjunction an all-negative support clause?*)
336 fun is_negative th = forall (not o #1) (literals (prop_of th));
338 val neg_clauses = List.filter is_negative;
341 (***** MESON PROOF PROCEDURE *****)
343 fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi,
344 As) = rhyps(phi, A::As)
345 | rhyps (_, As) = As;
347 (** Detecting repeated assumptions in a subgoal **)
349 (*The stringtree detects repeated assumptions.*)
350 fun ins_term (net,t) = Net.insert_term (op aconv) (t,t) net;
352 (*detects repetitions in a list of terms*)
353 fun has_reps [] = false
354 | has_reps [_] = false
355 | has_reps [t,u] = (t aconv u)
356 | has_reps ts = (Library.foldl ins_term (Net.empty, ts); false)
357 handle Net.INSERT => true;
359 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
360 fun TRYING_eq_assume_tac 0 st = Seq.single st
361 | TRYING_eq_assume_tac i st =
362 TRYING_eq_assume_tac (i-1) (eq_assumption i st)
363 handle THM _ => TRYING_eq_assume_tac (i-1) st;
365 fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st;
367 (*Loop checking: FAIL if trying to prove the same thing twice
368 -- if *ANY* subgoal has repeated literals*)
370 if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
371 then Seq.empty else Seq.single st;
374 (* net_resolve_tac actually made it slower... *)
375 fun prolog_step_tac horns i =
376 (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
377 TRYALL_eq_assume_tac;
379 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
380 fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
382 fun size_of_subgoals st = foldr addconcl 0 (prems_of st);
385 (*Negation Normal Form*)
386 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
387 not_impD, not_iffD, not_allD, not_exD, not_notD];
389 fun make_nnf1 th = make_nnf1 (tryres(th, nnf_rls))
391 forward_res make_nnf1
392 (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
395 (*The simplification removes defined quantifiers and occurrences of True and False.
396 nnf_ss also includes the one-point simprocs,
397 which are needed to avoid the various one-point theorems from generating junk clauses.*)
399 [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True,
400 if_False, if_cancel, if_eq_cancel, cases_simp];
401 val nnf_extra_simps =
402 thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;
405 HOL_basic_ss addsimps nnf_extra_simps
406 addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc];
408 fun make_nnf th = th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
409 |> simplify nnf_ss (*But this doesn't simplify premises...*)
412 (*Pull existential quantifiers to front. This accomplishes Skolemization for
413 clauses that arise from a subgoal.*)
415 if not (has_conns ["Ex"] (prop_of th)) then th
416 else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
417 disj_exD, disj_exD1, disj_exD2])))
419 skolemize (forward_res skolemize
420 (tryres (th, [conj_forward, disj_forward, all_forward])))
421 handle THM _ => forward_res skolemize (th RS ex_forward);
424 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
425 The resulting clauses are HOL disjunctions.*)
426 fun make_clauses ths =
427 (sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths)));
430 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
433 (distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
435 (*Could simply use nprems_of, which would count remaining subgoals -- no
436 discrimination as to their size! With BEST_FIRST, fails for problem 41.*)
438 fun best_prolog_tac sizef horns =
439 BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
441 fun depth_prolog_tac horns =
442 DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
444 (*Return all negative clauses, as possible goal clauses*)
445 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
447 fun skolemize_prems_tac prems =
448 cut_facts_tac (map (skolemize o make_nnf) prems) THEN'
451 (*Expand all definitions (presumably of Skolem functions) in a proof state.*)
452 fun expand_defs_tac st =
453 let val defs = filter (can dest_equals) (#hyps (crep_thm st))
454 in LocalDefs.def_export false defs st end;
456 (*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions*)
457 fun MESON cltac i st =
459 (EVERY [rtac ccontr 1,
461 EVERY1 [skolemize_prems_tac negs,
462 METAHYPS (cltac o make_clauses)]) 1,
463 expand_defs_tac]) i st
464 handle TERM _ => no_tac st; (*probably from check_is_fol*)
466 (** Best-first search versions **)
468 (*ths is a list of additional clauses (HOL disjunctions) to use.*)
469 fun best_meson_tac sizef =
471 THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
472 (has_fewer_prems 1, sizef)
473 (prolog_step_tac (make_horns cls) 1));
475 (*First, breaks the goal into independent units*)
476 val safe_best_meson_tac =
477 SELECT_GOAL (TRY Safe_tac THEN
478 TRYALL (best_meson_tac size_of_subgoals));
480 (** Depth-first search version **)
482 val depth_meson_tac =
483 MESON (fn cls => EVERY [resolve_tac (gocls cls) 1,
484 depth_prolog_tac (make_horns cls)]);
487 (** Iterative deepening version **)
489 (*This version does only one inference per call;
490 having only one eq_assume_tac speeds it up!*)
491 fun prolog_step_tac' horns =
492 let val (horn0s, hornps) = (*0 subgoals vs 1 or more*)
493 take_prefix Thm.no_prems horns
494 val nrtac = net_resolve_tac horns
495 in fn i => eq_assume_tac i ORELSE
496 match_tac horn0s i ORELSE (*no backtracking if unit MATCHES*)
497 ((assume_tac i APPEND nrtac i) THEN check_tac)
500 fun iter_deepen_prolog_tac horns =
501 ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
503 fun iter_deepen_meson_tac ths =
505 case (gocls (cls@ths)) of
506 [] => no_tac (*no goal clauses*)
508 (THEN_ITER_DEEPEN (resolve_tac goes 1)
510 (prolog_step_tac' (make_horns (cls@ths)))));
512 fun meson_claset_tac ths cs =
513 SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
515 val meson_tac = CLASET' (meson_claset_tac []);
518 (**** Code to support ordinary resolution, rather than Model Elimination ****)
520 (*Convert a list of clauses (disjunctions) to meta-level clauses (==>),
521 with no contrapositives, for ordinary resolution.*)
523 (*Rules to convert the head literal into a negated assumption. If the head
524 literal is already negated, then using notEfalse instead of notEfalse'
525 prevents a double negation.*)
526 val notEfalse = read_instantiate [("R","False")] notE;
527 val notEfalse' = rotate_prems 1 notEfalse;
529 fun negated_asm_of_head th =
530 th RS notEfalse handle THM _ => th RS notEfalse';
532 (*Converting one clause*)
533 fun make_meta_clause th =
534 negated_asm_of_head (make_horn resolution_clause_rules (check_is_fol th));
536 fun make_meta_clauses ths =
538 (distinct Drule.eq_thm_prop (map make_meta_clause ths));
540 (*Permute a rule's premises to move the i-th premise to the last position.*)
542 let val n = nprems_of th
543 in if 1 <= i andalso i <= n
544 then Thm.permute_prems (i-1) 1 th
545 else raise THM("select_literal", i, [th])
548 (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
550 val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
552 (*Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
553 fun select_literal i cl = negate_head (make_last i cl);
556 (*Top-level Skolemization. Allows part of the conversion to clauses to be
557 expressed as a tactic (or Isar method). Each assumption of the selected
558 goal is converted to NNF and then its existential quantifiers are pulled
559 to the front. Finally, all existential quantifiers are eliminated,
560 leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
561 might generate many subgoals.*)
563 fun skolemize_tac i st =
564 let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1))
567 (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1
568 THEN REPEAT (etac exE 1))),
569 REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st
571 handle Subscript => Seq.empty;
573 (*Top-level conversion to meta-level clauses. Each clause has
574 leading !!-bound universal variables, to express generality. To get
575 disjunctions instead of meta-clauses, remove "make_meta_clauses" below.*)
576 val make_clauses_tac =
579 let val ts = Logic.strip_assums_hyp prop
584 (map forall_intr_vars
585 (make_meta_clauses (make_clauses hyps))) 1)),
586 REPEAT_DETERM_N (length ts) o (etac thin_rl)]
590 (*** setup the special skoklemization methods ***)
592 (*No CHANGED_PROP here, since these always appear in the preamble*)
594 val skolemize_meth = Method.SIMPLE_METHOD' HEADGOAL skolemize_tac;
596 val make_clauses_meth = Method.SIMPLE_METHOD' HEADGOAL make_clauses_tac;
598 val skolemize_setup =
600 [("skolemize", Method.no_args skolemize_meth,
601 "Skolemization into existential quantifiers"),
602 ("make_clauses", Method.no_args make_clauses_meth,
603 "Conversion to !!-quantified meta-level clauses")];
607 structure BasicMeson: BASIC_MESON = Meson;